Lint to mathlib standards

Author: YaelDillies

LeanAPAP/FiniteField.lean

@@ -21,7 +21,7 @@ open Finset hiding card
 open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise mu
 
 universe u
-variable {G : Type u} [AddCommGroup G] [DecidableEq G] [Fintype G] {A C : Finset G} {x y γ ε : ℝ}
+variable {G : Type u} [AddCommGroup G] [Fintype G] {A C : Finset G} {x y γ ε : ℝ}
 
 local notation "𝓛" x:arg => 1 + log x⁻¹
 
@@ -37,6 +37,7 @@ private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by
   have : 0 ≤ log x⁻¹ := by bound
   positivity
 
+set_option linter.flexible false in
 private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by
   obtain rfl | hx₀ := hx₀.eq_or_lt
   · simp; positivity
@@ -87,8 +88,9 @@ private lemma curlog_rpow_le (hx₀ : 0 < x) (hy : 1 ≤ y) : 𝓛 (x ^ y) ≤ y
 private lemma curlog_pow_le {n : ℕ} (hx₀ : 0 < x) (hn : n ≠ 0) : 𝓛 (x ^ n) ≤ n * 𝓛 x := by
   rw [← rpow_natCast]; exact curlog_rpow_le hx₀ <| mod_cast Nat.one_le_iff_ne_zero.2 hn
 
-lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.Nonempty)
-    (hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
+lemma global_dichotomy [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G]
+    (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
+    (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ε / (2 * card G) ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), μ univ] := by
   have hC : C.Nonempty := by simpa using hγ.trans_le hγC
   have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
@@ -140,8 +142,9 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
 
 variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ}
 
-lemma ap_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε)
-    (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
+set_option linter.flexible false in
+lemma ap_in_ff [DecidableEq G] (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹)
+    (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ 2 ^ 32 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 ∧
           |∑ x ∈ S, (μ (Set.toFinset V) ∗ μ A₁ ∗ μ A₂) x - ∑ x ∈ S, (μ A₁ ∗ μ A₂) x| ≤ ε := by
@@ -237,16 +240,18 @@ lemma ap_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α 
     have : ∑ x ∈ S, (μ_[ℝ] A₁ ∗ μ A₂) x = (μ_[ℝ] A₁ ∗ μ A₂ ○ 𝟭 S) 0 := by simp [dconv_indicate]
     sorry
 
-lemma ap_in_ff' (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε)
-    (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
+lemma ap_in_ff' [DecidableEq G] (hq₃ : 3 ≤ q) (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹)
+    (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ 2 ^ 32 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 ∧
           |∑ x ∈ S, (μ (Set.toFinset V) ∗ μ A₁ ○ μ A₂) x - ∑ x ∈ S, (μ A₁ ○ μ A₂) x| ≤ ε := by
   simpa [← conjneg_mu] using ap_in_ff S hq₃ hq (A₂ := -A₂) hα₀ hα₂ hε₀ hε₁ hαA₁ (by simpa)
 
+set_option linter.flexible false in
 set_option maxHeartbeats 400000 in
-lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (hq : q.Prime)
-    (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
+-- FIXME: Get rid of raised heartbeats
+lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
+    (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < 1) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
     (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ μ A, μ C⟫_[ℝ] - 1|) :
     ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
         ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
@@ -446,6 +451,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
         · exact conv_nonneg mu_nonneg mu_nonneg
         · exact mu_nonneg
 
+set_option linter.flexible false in
 theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFree (α := G) A) :
     finrank (ZMod q) G ≤ 2 ^ 156 * 𝓛 A.dens ^ 9 := by
   let n : ℝ := finrank (ZMod q) G
@@ -487,6 +493,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction i with
     | zero =>
+      classical
       exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,
         by simp [α], by simp [α, nnratCast_dens]⟩
     | succ i ih =>
@@ -520,7 +527,6 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
       · congr 1 with x
         simp
       · simp
-    simp at hx
     refine ⟨V', inferInstance, inferInstance, inferInstance, inferInstance, B', ?_, ?_, ?_,
       fun h ↦ ?_⟩
     · calc

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -76,7 +76,7 @@ lemma my_other_markov (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g
   classical
   rw [one_sub_mul, sub_le_comm, ← cast_card_sdiff (filter_subset _ A), ← filter_not,
     filter_false_of_mem]
-  · simp; positivity
+  · simp only [card_empty, CharP.cast_eq_zero]; positivity
   intro i hi
   rw [(sum_eq_zero_iff_of_nonneg hg).1 (h.antisymm (sum_nonneg hg)) i hi]
   simp

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -191,7 +191,7 @@ noncomputable instance [Finite G] : SupSet (BohrSet G) where
     mem_frequencies := by simp
   }
 
-lemma iInf_lt_top {α β : Type*} [CompleteLattice β] {S : Set α} {f : α → β}:
+lemma iInf_lt_top {α β : Type*} [CompleteLattice β] {S : Set α} {f : α → β} :
     (⨅ i ∈ S, f i) < ⊤ ↔ ∃ i ∈ S, f i < ⊤ := by
   simp [lt_top_iff_ne_top]
 
@@ -257,8 +257,6 @@ lemma nnreal_smul_ne_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x 
     by_contra hy
     simp [hy, ENNReal.smul_top, hx] at h
 
-open scoped Classical
-
 noncomputable instance instSMul : SMul ℝ (BohrSet G) where
   smul ρ B := BohrSet.mk B.frequencies
       (fun ψ => if ψ ∈ B.frequencies then Real.nnabs ρ * B.ewidth ψ else ⊤) fun ψ => by
@@ -342,7 +340,6 @@ lemma smul_add_smul_subset [Finite G] {B : BohrSet G} {ρ₁ ρ₂ : ℝ} (hρ
   add_subset_of_ewidth fun ψ => by
     simp only [Pi.add_apply, ewidth_smul]; split <;> simp [add_nonneg, add_mul, *]
 
-
 end BohrSet
 
 -- variable {ρ : ℝ}

LeanAPAP/Prereqs/Chang.lean

@@ -25,7 +25,7 @@ private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by
 
 private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by
   obtain rfl | hx₀ := hx₀.eq_or_lt
-  · simp; positivity
+  · simp only [inv_zero, log_zero, add_zero, inv_one, rpow_one]; positivity
   obtain rfl | hx₁ := hx₁.eq_or_lt
   · simp
   have hx := (one_lt_inv₀ hx₀).2 hx₁

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -241,7 +241,7 @@ lemma IsSelfAdjoint.cconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelf
 lemma IsSelfAdjoint.cdconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ₙ g) :=
   (conj_cdconv _ _).trans <| congr_arg₂ _ hf hg
 
-@[simp]lemma conjneg_cconv (f g : G → R) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g := by
+@[simp] lemma conjneg_cconv (f g : G → R) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g := by
   funext a
   simp only [cconv_apply, conjneg_apply, map_expect, map_mul]
   exact Finset.expect_equiv (Equiv.neg (G × G)) (by simp [eq_comm, ← neg_eq_iff_eq_neg, add_comm])

LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean

@@ -228,7 +228,7 @@ lemma IsSelfAdjoint.conv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfA
 lemma IsSelfAdjoint.dconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ g) :=
   (conj_dconv _ _).trans <| congr_arg₂ _ hf hg
 
-@[simp]lemma conjneg_conv (f g : G → R) : conjneg (f ∗ g) = conjneg f ∗ conjneg g := by
+@[simp] lemma conjneg_conv (f g : G → R) : conjneg (f ∗ g) = conjneg f ∗ conjneg g := by
   funext a
   simp only [conv_apply, conjneg_apply, map_sum, map_mul]
   exact sum_equiv (Equiv.neg _) (by simp [← neg_eq_iff_eq_neg, add_comm]) (by simp)

LeanAPAP/Prereqs/Convolution/Norm.lean

@@ -95,7 +95,6 @@ lemma dLpNorm_conv_le {p : ℝ≥0} (hp : 1 ≤ p) (f g : G → 𝕜) : ‖f ∗
       simp
     · have : 1 - (p : ℝ)⁻¹ ≠ 0 := sub_ne_zero.2 (inv_ne_one.2 <| NNReal.coe_ne_one.2 hp.ne').symm
       simp [NNReal.mul_rpow, hp₀.ne', this]
-
   calc
     ∑ x, ‖∑ y, f y * g (x - y)‖₊ ^ (p : ℝ) ≤
         ∑ x, (∑ y, ‖f y‖₊ ^ (p : ℝ) * ‖g (x - y)‖₊) * (∑ y, ‖g (x - y)‖₊) ^ (p - 1 : ℝ) :=

LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean

@@ -322,7 +322,7 @@ lemma dLpNorm_eq_dL1Norm_rpow (hp : p ≠ 0) (f : α → 𝕜) :
 lemma dLpNorm_rpow' {p : ℝ≥0∞} (hp₀ : p ≠ 0) (hp : p ≠ ∞) (hq : q ≠ 0) (f : α → 𝕜) :
     ‖f‖_[p] ^ (q : ℝ) = ‖(fun a ↦ ‖f a‖) ^ (q : ℝ)‖_[p / q] := by
   lift p to ℝ≥0 using hp
-  simp at hp₀
+  simp only [ne_eq, ENNReal.coe_eq_zero] at hp₀
   rw [← ENNReal.coe_div hq, dLpNorm_rpow (div_ne_zero hp₀ hq) hq (fun _ ↦ norm_nonneg _),
     dLpNorm_norm, ← ENNReal.coe_mul, div_mul_cancel₀ _ hq]
 

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -65,7 +65,7 @@ private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a 
 -- when the corresponding ε is -1
 -- but the order here is a bit subtle (ie this explanation is an oversimplification)
 private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ)
-    (hε : ε ∈ ({-1, 1} : Finset ℝ)^^n) (g : (Fin n → ℝ) → ℝ) :
+    (hε : ε ∈ ({-1, 1} : Finset ℝ) ^^ n) (g : (Fin n → ℝ) → ℝ) :
     ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, g (ε * (f ∘ a - f ∘ b)) =
       ∑ a ∈ A ^^ n, ∑ b ∈ A ^^ n, g (f ∘ a - f ∘ b) := by
   rw [← sum_product', ← sum_product']

LeanAPAP/Prereqs/Rudin.lean

@@ -76,7 +76,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : G → ℂ) (hf : AddDissociated
   have : (‖re ∘ f‖ₙ_[↑p] / p) ^ p ≤ (2 * exp 2⁻¹) ^ p := by
     calc
       _ = 𝔼 a, |(f a).re| ^ p / p ^ p := by
-          simp [div_pow, cLpNorm_pow_eq_expect_norm hp₀]; rw [expect_div]
+          simp [div_pow, cLpNorm_pow_eq_expect_norm hp₀, expect_div]
       _ ≤ 𝔼 a, |(f a).re| ^ p / p ! := by gcongr; norm_cast; exact p.factorial_le_pow
       _ ≤ 𝔼 a, exp |(f a).re| := by gcongr; exact pow_div_factorial_le_exp _ (abs_nonneg _) _
       _ ≤ _ := rudin_exp_abs_ineq f hf