Use dens more widely

LeanAPAP.lean

@@ -5,6 +5,7 @@ import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Mathlib.Data.Rat.Cast.Defs
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup

LeanAPAP/Extras/BSG.lean

@@ -33,7 +33,7 @@ lemma claim_one : ∑ s, (𝟭_[β] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card =
   simp only [←thing_three, ←thing_one_right, sq]
 
 lemma claim_two :
-    (E[A, B] : ℝ) ^ 2 / (A.card * B.card) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card ^ 2 := by
+    (E[A, B]) ^ 2 / (A.card * B.card) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card ^ 2 := by
   let f := fun s ↦ ((𝟭_[ℝ] A ○ 𝟭 B) s).sqrt
   have hf : ∀ s, f s ^ 2 = (𝟭_[ℝ] A ○ 𝟭 B) s := by
     intro s
@@ -204,7 +204,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
   rw [mul_assoc]
   gcongr _ * ?_
   field_simp [hA, hB, hK, le_div_iff, div_le_iff] at hE ⊢
-  convert_to ((A.card : ℝ) ^ 2 * B.card) ^ 2 ≤ (E[A, B] * K) ^ 2
+  convert_to (A.card ^ 2 * B.card) ^ 2 ≤ (E[A, B] * K) ^ 2
   · ring_nf
   · ring_nf
   gcongr

LeanAPAP/FiniteField/Basic.lean

@@ -1,3 +1,4 @@
+import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Physics.Unbalancing
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.FourierTransform.Compact
@@ -12,15 +13,15 @@ open scoped NNReal
 
 variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G] {A C : Finset G} {γ ε : ℝ}
 
-lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ : 0 < γ)
+lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
     (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ε / (2 * card G) ≤
       ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] := by
   have hC : C.Nonempty := by
     rw [nonempty_iff_ne_empty]
     rintro rfl
     simp [hγ.not_le] at hγC
-  have hγ₁ : γ ≤ 1 := hγC.trans (div_le_one_of_le (Nat.cast_le.2 C.card_le_univ) $ by positivity)
+  have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
   set p := 2 * ⌈γ.curlog⌉₊
   have hp : 1 < p :=
     Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ hγ₁)
@@ -42,7 +43,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
       expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ← mul_inv_cancel, ← mul_sub,
       abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity
   · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow]
-    rw [le_div_iff, mul_comm] at hγC
+    rw [cast_dens, le_div_iff, mul_comm] at hγC
     refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_)
     all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two, p]
@@ -62,15 +63,15 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
 
 variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ}
 
-lemma ap_in_ff (hA₁ : α ≤ A₁.card / card G) (hA₂ : α ≤ A₂.card / card G) :
+lemma ap_in_ff (hA₁ : α ≤ A₁.dens) (hA₂ : α ≤ A₂.dens) :
     ∃ (V : Submodule (ZMod q) G) (V' : Finset G),
       (V : Set G) = V' ∧
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
             2 ^ 27 * α.curlog ^ 2 * (ε * α).curlog ^ 2 / ε ^ 2 ∧
           |∑ x in S, (μ V' ∗ μ A₁ ∗ μ A₂) x - ∑ x in S, (μ A₁ ∗ μ A₂) x| ≤ ε :=
   sorry
 
-lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card G) (hγC : γ ≤ C.card / card G)
+lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.dens) (hγC : γ ≤ C.dens)
     (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ∃ (V : Submodule (ZMod q) G) (V' : Finset G),
       (V : Set G) = V' ∧
@@ -85,7 +86,7 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card
       Nat.cast_zero, indicate_empty, zero_mul, lpNorm_zero, true_and_iff,
       Finset.card_empty, zero_div] at hαA ⊢
     exact ⟨by positivity, mul_nonpos_of_nonneg_of_nonpos (by positivity) hαA⟩
-  have hγ₁ : γ ≤ 1 := hγC.trans (div_le_one_of_le (Nat.cast_le.2 C.card_le_univ) $ by positivity)
+  have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
   have hG : (card G : ℝ) ≠ 0 := by positivity
   have := unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ hγ₁).ne') (ε / 2)
     (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num)

LeanAPAP/Mathlib/Data/Finset/Density.lean

@@ -0,0 +1,17 @@
+import Mathlib.Data.Finset.Density
+import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
+
+open Fintype
+
+namespace Finset
+variable {α 𝕜 : Type*} [Fintype α] {s : Finset α}
+
+@[simp] lemma dens_le_one : s.dens ≤ 1 := by
+  cases isEmpty_or_nonempty α
+  · simp [Subsingleton.elim s ∅]
+  · simpa using dens_le_dens s.subset_univ
+
+lemma cast_dens [Semifield 𝕜] [CharZero 𝕜] (s : Finset α) :
+    (s.dens : 𝕜) = s.card / Fintype.card α := by simp [dens]
+
+end Finset

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -129,11 +129,8 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
   simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
 
 lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
-    (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k,
-          ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
-      (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
+    (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
+      (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
   -- lots of the equalities about m can be automated but it's *way* slower
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
   have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1
@@ -150,8 +147,8 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
   refine (lpNorm_conv_le this.le _ _).trans ?_
   rw [l1Norm_mu hA, mul_one]
 
-lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m)  (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :
-    (8 * m : ℝ) ^ m * k ^ (m - 1) * A.card ^ k * k * (2 * ‖f‖_[2 * m]) ^ (2 * m) ≤
+lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m)  (hk : 64 * m / ε ^ 2 ≤ k) :
+    (8 * m) ^ m * k ^ (m - 1) * A.card ^ k * k * (2 * ‖f‖_[2 * m]) ^ (2 * m) ≤
       1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * ↑A.card ^ k := by
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
   have hm' : 2 * m ≠ 0 := by
@@ -208,10 +205,8 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
     simp only [Pi.sub_apply, translate_apply]
   simp only [this]
   have :
-    (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
-      (8 * m : ℝ) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
+    (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
+      (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
     lemma28_part_two hm hA
   refine this.trans ?_
   simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow]
@@ -478,7 +473,6 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
   refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩
   set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C
   have hT' : T.Nonempty := by
-    have := hS.card_pos -- TODO: positivity
     have : (0 : ℝ) < T.card := hKT.trans_lt' $ by positivity
     simpa [card_pos] using this
   calc

LeanAPAP/Physics/DRC.lean

@@ -1,3 +1,4 @@
+import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
@@ -229,15 +230,15 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
     (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hA : A.Nonempty)
     (hf : ∃ x, x ∈ A - A ∧ (𝟭 A ○ 𝟭 A) x ≤ (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ]) :
     ∃ A₁ A₂, 1 - δ ≤ ∑ x in s p ε univ univ A, (μ A₁ ○ μ A₂) x ∧
-        (4 : ℝ)⁻¹ * (A.card / card G : ℝ) ^ (2 * p) ≤ A₁.card / card G ∧
-          (4 : ℝ)⁻¹ * (A.card / card G : ℝ) ^ (2 * p) ≤ A₂.card / card G := by
+        (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₁.dens ∧
+          (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₂.dens := by
   have hp₀ : p ≠ 0 := by positivity
   have :
-    (4 : ℝ)⁻¹ * (A.card / card G) ^ (2 * p) ≤
+    (4 : ℝ)⁻¹ * (A.dens) ^ (2 * p) ≤
       4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / A.card ^ (2 * p) := by
     rw [mul_div_assoc, ←div_pow]
     refine mul_le_mul_of_nonneg_left (pow_le_pow_left (by positivity) ?_ _) (by norm_num)
-    rw [le_div_iff, ←mul_div_right_comm]
+    rw [cast_dens, le_div_iff, ←mul_div_right_comm]
     calc
       _ = ‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] := by
         simp [mu, wlpNorm_smul_right, hp₀, l1Norm_dconv, card_univ, inv_mul_eq_div]

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -18,7 +18,7 @@ section NormedAddCommGroup
 variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p q : ℝ≥0∞} {f g h : ∀ i, α i}
 
 /-- The Lp norm of a function with the compact normalisation. -/
-noncomputable def nlpNorm (p : ℝ≥0∞) (f : ∀ i, α i) : ℝ := ‖f‖_[p] / (card ι : ℝ) ^ p.toReal⁻¹
+noncomputable def nlpNorm (p : ℝ≥0∞) (f : ∀ i, α i) : ℝ := ‖f‖_[p] / card ι ^ p.toReal⁻¹
 
 notation "‖" f "‖ₙ_[" p "]" => nlpNorm p f
 

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -83,7 +83,7 @@ variable {α β : Type*} [RCLike β] [Fintype α] [DecidableEq α] {s : Finset 
 
 lemma lpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p] ^ (p : ℝ) = s.card := by
   have : ∀ x, (ite (x ∈ s) 1 0 : ℝ) ^ (p : ℝ) =
-    ite (x ∈ s) ((1 : ℝ) ^ (p : ℝ) : ℝ) ((0 : ℝ) ^ (p : ℝ)) := fun x ↦ by split_ifs <;> simp
+    ite (x ∈ s) (1 ^ (p : ℝ)) (0 ^ (p : ℝ)) := fun x ↦ by split_ifs <;> simp
   simp [lpNorm_rpow_eq_sum, hp, indicate_apply, apply_ite Norm.norm, -sum_const, card_eq_sum_ones,
     sum_boole, this, zero_rpow, filter_mem_eq_inter]
 

LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean

@@ -146,8 +146,7 @@ section NormedAddCommGroup
 variable {α : Type*} [NormedAddCommGroup α] {p : ℝ≥0}
 
 @[simp]
-lemma lpNorm_const (hp : p ≠ 0) (a : α) :
-    ‖const ι a‖_[p] = (Fintype.card ι : ℝ) ^ (p⁻¹ : ℝ) * ‖a‖ := by
+lemma lpNorm_const (hp : p ≠ 0) (a : α) : ‖const ι a‖_[p] = Fintype.card ι ^ (p⁻¹ : ℝ) * ‖a‖ := by
   simp only [lpNorm_eq_sum hp, card_univ, mul_rpow, norm_nonneg, rpow_nonneg,
     NNReal.coe_ne_zero.2 hp, rpow_rpow_inv, const_apply, sum_const, nsmul_eq_mul, Nat.cast_nonneg,
     Ne, not_false_iff]

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -152,7 +152,7 @@ private lemma step_seven {f : ι → ℝ} {a b : Fin n → ι} :
   exact add_sq_le.trans_eq (by simp)
 
 private lemma step_eight {f : ι → ℝ} {a b : Fin n → ι} :
-    m ^ m * 2 ^ m * (∑ i, (f (a i) ^ 2 + f (b i) ^ 2) : ℝ) ^ m ≤
+    m ^ m * 2 ^ m * (∑ i, (f (a i) ^ 2 + f (b i) ^ 2)) ^ m ≤
       m ^ m * 2 ^ (m + (m - 1)) *
         ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) := by
   rw [pow_add, ← mul_assoc _ _ (2 ^ _), mul_assoc _ (2 ^ (m - 1)), sum_add_distrib]