Bump mathlib

LeanAPAP.lean

@@ -2,34 +2,20 @@ import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Mathlib.Algebra.Group.Basic
-import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset
-import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Floor
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
-import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
-import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Preimage
-import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
-import LeanAPAP.Mathlib.Order.CompleteLattice
 import LeanAPAP.Mathlib.Order.Hom.Basic
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
@@ -73,6 +59,5 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
-import LeanAPAP.Prereqs.PointwiseDensity
 import LeanAPAP.Prereqs.Randomisation
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/FiniteField.lean

@@ -1,17 +1,11 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
-import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
-import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.Inner.Function
-import LeanAPAP.Prereqs.PointwiseDensity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
@@ -22,7 +16,7 @@ import LeanAPAP.Physics.Unbalancing
 
 set_option linter.haveLet 0
 
-attribute [-simp] div_pow Real.log_inv
+attribute [-simp] Real.log_inv
 
 open FiniteDimensional Fintype Function Real MeasureTheory
 open Finset hiding card
@@ -188,10 +182,10 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
         _ ≤ 2 ^ 12 * 𝓛 α * (2 * 𝓛 α) * (2 ^ 3 * 𝓛 (ε * α)) ^ 2 / ε ^ 2 := by
           gcongr
           · exact le_add_of_nonneg_left zero_le_one
-          · exact (Int.ceil_lt_two_mul $ one_le_curlog hα₀.le hα₁).le
+          · exact Int.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog hα₀.le hα₁
           · calc
               k ≤ 2 * 𝓛 (ε * α / 4) :=
-                (Nat.ceil_lt_two_mul $ one_le_curlog (by positivity) sorry).le
+                Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity) sorry
               _ ≤ 2 * (4 * 𝓛 (ε * α)) := by
                 gcongr
                 exact curlog_div_le (by positivity) (mul_le_one hε₁ hα₀.le hα₁) (by norm_num)
@@ -211,11 +205,14 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
         · calc
             exp 1 ^ 2 ≤ 2.7182818286 ^ 2 := by gcongr; exact exp_one_lt_d9.le
             _ ≤ 2 ^ 3 := by norm_num
-        · exact (Nat.ceil_lt_two_mul $ one_le_curlog (by positivity) $ mod_cast T.dens_le_one).le
+        · exact Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <|
+            one_le_curlog (by positivity) <| mod_cast T.dens_le_one
       _ = ⌈2 ^ 11 * 𝓛 T.dens⌉₊ := by ring_nf
-      _ ≤ 2 * (2 ^ 11 * 𝓛 T.dens) :=
-        (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le (by norm_num) $
-          one_le_curlog (by positivity) $ mod_cast T.dens_le_one).le
+      _ ≤ 2 * (2 ^ 11 * 𝓛 T.dens) := Nat.ceil_le_two_mul <|
+          calc
+            (2⁻¹ : ℝ) ≤ 2 ^ 11 * 1 := by norm_num
+            _ ≤ 2 ^ 11 * 𝓛 T.dens := by
+              gcongr; exact one_le_curlog (by positivity) $ mod_cast T.dens_le_one
       _ = 2 ^ 12 * 𝓛 T.dens := by ring
       _ ≤ 2 ^ 12 * (1 + 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by gcongr
       _ ≤ 2 ^ 12 * (2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 +
@@ -284,12 +281,16 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
         gcongr
         · assumption
         · norm_num
-        · exact (Nat.ceil_lt_two_mul ‹_›).le
+        · exact Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans ‹_›
       _ = 2 * ⌈2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ⌉₊ := by ring_nf
       _ ≤ 2 * (2 * (2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ)) := by
         gcongr
-        exact (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le
-          (by norm_num) $ one_le_pow₀ (one_le_inv hε₀ hε₁.le) _) ‹_›).le
+        refine Nat.ceil_le_two_mul ?_
+        calc
+          (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num
+          _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_
+        gcongr
+        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le) _
       _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring
   obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),
       1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -1,7 +1,6 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Expect.Complex
@@ -451,7 +450,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
           calc
             _ ≤ 2.7182818286 ^ 2 := pow_le_pow_left (by positivity) exp_one_lt_d9.le _
             _ ≤ _ := by norm_num
-      _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm]
+      _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]
       _ ≤ _ := hKT
   set F : G → ℂ := τ t (μ A ∗ 𝟭 B) - μ A ∗ 𝟭 B
   have (x) :=

LeanAPAP/Physics/DRC.lean

@@ -122,7 +122,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
       ≤ (A₁ s).card / B₁.card * ((A₂ s).card / B₂.card) := by
       rw [div_mul_div_comm, le_div_iff₀]
-      simpa [hg_def, hM_def, mul_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
+      simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
         mul_div_right_comm] using h
       positivity
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
@@ -258,7 +258,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
         _ ≤ _ := wLpNorm_mono_right (one_le_two.trans $ by norm_cast) _ _
       · exact Nat.cast_pos.2 hA.card_pos
     obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ :=
-      sifting univ univ hε hε₁ hδ hp hp₂ hpε (by simp [univ_nonempty]) hA (by simpa)
+      sifting univ univ hε hε₁ hδ hp hp₂ hpε (by simp) hA (by simpa)
     exact ⟨A₁, A₂, h, this.trans $ by simpa [nnratCast_dens] using hcard₁,
       this.trans $ by simpa [nnratCast_dens] using hcard₂⟩
   · refine ⟨A, A, ?_, ?_⟩

LeanAPAP/Physics/Unbalancing.lean

@@ -1,7 +1,5 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Algebra.Order.Floor
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
@@ -217,10 +215,19 @@ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁
   · calc
       (⌈120 / ε * log (3 / ε) * p⌉₊ : ℝ)
         = ⌈120 * ε⁻¹ * log (3 * ε⁻¹) * p⌉₊ := by simp [div_eq_mul_inv]
-      _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) :=
-        (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le
-          (one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le (by norm_num) $
-            one_le_inv hε₀ hε₁) $ sorry) $ by simpa [Nat.one_le_iff_ne_zero]).le
+      _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) := Nat.ceil_le_two_mul <|
+        calc
+          (2⁻¹ : ℝ) ≤ 120 * 1 * 1 * 1 := by norm_num
+          _ ≤ 120 * ε⁻¹ * log (3 * ε⁻¹) * p := by
+            gcongr
+            · exact one_le_inv hε₀ hε₁
+            · rw [← log_exp 1]
+              gcongr
+              calc
+                exp 1 ≤ 2.7182818286 := exp_one_lt_d9.le
+                _ ≤ 3 * 1 := by norm_num
+                _ ≤ 3 * ε⁻¹ := by gcongr; exact one_le_inv hε₀ hε₁
+            · exact mod_cast hp
       _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity)
       _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num
       _ = 2 ^ 10 * ε⁻¹ ^ 2 * p := by ring

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -25,7 +25,7 @@ variable [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
 
 lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 := by
   split_ifs with h
-  · simp [h, card_univ, univ_nonempty]
+  · simp [h, card_univ]
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
   refine eq_zero_of_mul_eq_self_left hx ?_
   rw [Finset.mul_expect]

LeanAPAP/Prereqs/Balance.lean

@@ -38,7 +38,7 @@ lemma balance_apply (f : ι → α) (x : ι) : balance f x = f x - 𝔼 y, f y :
 @[simp] lemma expect_balance (f : ι → α) : 𝔼 x, balance f x = 0 := by simp [expect]
 
 @[simp] lemma balance_idem (f : ι → α) : balance (balance f) = balance f := by
-  cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib, univ_nonempty]
+  cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib]
 
 @[simp] lemma map_balance {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0 α β] (g : F) (f : ι → α)
     (a : ι) : g (balance f a) = balance (g ∘ f) a := by simp [balance, map_expect]

LeanAPAP/Prereqs/Chang.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex

LeanAPAP/Prereqs/NNLpNorm.lean

@@ -1,8 +1,8 @@
 import Mathlib.Algebra.BigOperators.Expect
+import Mathlib.Algebra.Order.Module.Rat
 import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
-import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 
 open Filter