From 7700190ef8ffb0a8e9fc3870a5309ad366c0bdc6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 28 Sep 2024 17:42:37 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 14 -------- LeanAPAP/FiniteField.lean | 32 ++++++++++--------- LeanAPAP/Mathlib/Algebra/Group/Basic.lean | 5 --- .../Algebra/Group/Pointwise/Finset.lean | 11 ------- .../Mathlib/Algebra/Group/Subgroup/Basic.lean | 3 -- LeanAPAP/Mathlib/Algebra/Order/Floor.lean | 32 ------------------- .../Mathlib/Algebra/Order/Module/Rat.lean | 12 ------- LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean | 4 --- .../Analysis/SpecialFunctions/Log/Basic.lean | 11 ------- .../Analysis/SpecialFunctions/Pow/Real.lean | 16 ---------- .../Combinatorics/Additive/FreimanHom.lean | 10 ------ LeanAPAP/Mathlib/Data/Finset/Preimage.lean | 10 ------ LeanAPAP/Mathlib/Data/Fintype/Basic.lean | 3 -- .../Mathlib/MeasureTheory/Measure/Count.lean | 5 --- LeanAPAP/Mathlib/Order/CompleteLattice.lean | 6 ---- LeanAPAP/Physics/AlmostPeriodicity.lean | 3 +- LeanAPAP/Physics/DRC.lean | 4 +-- LeanAPAP/Physics/Unbalancing.lean | 19 +++++++---- LeanAPAP/Prereqs/AddChar/Basic.lean | 2 +- LeanAPAP/Prereqs/Balance.lean | 2 +- LeanAPAP/Prereqs/Chang.lean | 1 - LeanAPAP/Prereqs/Convolution/Compact.lean | 1 - LeanAPAP/Prereqs/NNLpNorm.lean | 2 +- LeanAPAP/Prereqs/PointwiseDensity.lean | 11 ------- lake-manifest.json | 6 ++-- 25 files changed, 39 insertions(+), 186 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Algebra/Group/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Floor.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean delete mode 100644 LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean delete mode 100644 LeanAPAP/Mathlib/Combinatorics/Additive/FreimanHom.lean delete mode 100644 LeanAPAP/Mathlib/Data/Finset/Preimage.lean delete mode 100644 LeanAPAP/Mathlib/Data/Fintype/Basic.lean delete mode 100644 LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean delete mode 100644 LeanAPAP/Mathlib/Order/CompleteLattice.lean delete mode 100644 LeanAPAP/Prereqs/PointwiseDensity.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index efb7e390b1..efb7c9be95 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -2,34 +2,21 @@ 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 +60,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 diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index 0e0a9daaf7..b00f6970f9 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -1,17 +1,12 @@ 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 +17,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 +183,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 +206,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 +282,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 ∧ diff --git a/LeanAPAP/Mathlib/Algebra/Group/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Basic.lean deleted file mode 100644 index e81bd99784..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Group/Basic.lean +++ /dev/null @@ -1,5 +0,0 @@ -/-! -# TODO - -Unsimp `div_pow`/`zsmul_sub` --/ diff --git a/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean deleted file mode 100644 index dca272e63f..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Mathlib.Algebra.Group.Pointwise.Finset.Basic -import Mathlib.Data.Finset.Density - -open scoped Pointwise - -namespace Finset -variable {α : Type*} [DecidableEq α] [InvolutiveInv α] [Fintype α] - -@[to_additive (attr := simp)] lemma dens_inv (s : Finset α) : s⁻¹.dens = s.dens := by simp [dens] - -end Finset diff --git a/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean deleted file mode 100644 index 5b2df3ffd4..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Mathlib.Algebra.Group.Subgroup.Basic - -attribute [simp] AddMonoidHom.mem_ker diff --git a/LeanAPAP/Mathlib/Algebra/Order/Floor.lean b/LeanAPAP/Mathlib/Algebra/Order/Floor.lean deleted file mode 100644 index a5017131ad..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Floor.lean +++ /dev/null @@ -1,32 +0,0 @@ -import Mathlib.Algebra.Order.Floor - -namespace Nat -variable {α : Type*} [LinearOrderedField α] [FloorSemiring α] {a b : α} - -lemma ceil_lt_mul (ha : 0 ≤ a) (hb : 1 < b) (h : (b - 1)⁻¹ ≤ a) : ⌈a⌉₊ < b * a := by - rw [← sub_pos] at hb - calc - ⌈a⌉₊ < a + 1 := ceil_lt_add_one ha - _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity - _ ≤ a + (b - 1) * a := by gcongr; positivity - _ = b * a := by rw [sub_one_mul, add_sub_cancel] - -lemma ceil_lt_two_mul (ha : 1 ≤ a) : ⌈a⌉₊ < 2 * a := - ceil_lt_mul (by positivity) one_lt_two (by norm_num; exact ha) - -end Nat - -namespace Int -variable {α : Type*} [LinearOrderedField α] [FloorRing α] {a b : α} - -lemma ceil_lt_mul (hb : 1 < b) (ha : (b - 1)⁻¹ ≤ a) : ⌈a⌉ < b * a := by - rw [← sub_pos] at hb - calc - ⌈a⌉ < a + 1 := ceil_lt_add_one _ - _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity - _ ≤ a + (b - 1) * a := by gcongr; positivity - _ = b * a := by rw [sub_one_mul, add_sub_cancel] - -lemma ceil_lt_two_mul (ha : 1 ≤ a) : ⌈a⌉ < 2 * a := ceil_lt_mul one_lt_two (by norm_num; exact ha) - -end Int diff --git a/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean deleted file mode 100644 index 61a408f06f..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Mathlib.Algebra.Order.Module.Defs -import Mathlib.Data.Rat.Cast.Order - -variable {α : Type*} - -instance [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] : PosSMulMono ℚ≥0 α where - elim a _ _b₁ _b₂ hb := (smul_le_smul_of_nonneg_left hb a.2 :) - -instance LinearOrderedSemifield.toPosSMulStrictMono [LinearOrderedSemifield α] : - PosSMulStrictMono ℚ≥0 α where - elim a ha b₁ b₂ hb := by - simp_rw [NNRat.smul_def]; exact mul_lt_mul_of_pos_left hb (NNRat.cast_pos.2 ha) diff --git a/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean b/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean deleted file mode 100644 index e495c938dd..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Mathlib.Algebra.Order.Ring.Cast - -@[gcongr] protected alias ⟨_, GCongr.intCast_mono⟩ := Int.cast_le -@[gcongr] protected alias ⟨_, GCongr.intCast_strictMono⟩ := Int.cast_lt diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean deleted file mode 100644 index a6a0b64853..0000000000 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Mathlib.Analysis.SpecialFunctions.Log.Basic - -namespace Real -variable {x : ℝ} - -lemma log_le_self (hx : 0 ≤ x) : log x ≤ x := by - obtain rfl | hx := hx.eq_or_lt - · simp - · exact (log_le_sub_one_of_pos hx).trans (by linarith) - -end Real diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean deleted file mode 100644 index 9ea8a11b05..0000000000 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ /dev/null @@ -1,16 +0,0 @@ -import Mathlib.Analysis.SpecialFunctions.Pow.Real - -namespace Real -variable {x : ℝ} - -lemma rpow_inv_log_le_exp_one : x ^ (log x)⁻¹ ≤ exp 1 := by - refine (le_abs_self _).trans ?_ - refine (Real.abs_rpow_le_abs_rpow _ _).trans ?_ - rw [← log_abs] - obtain hx | hx := (abs_nonneg x).eq_or_gt - · simp [hx] - · rw [rpow_def_of_pos hx] - gcongr - exact mul_inv_le_one - -end Real diff --git a/LeanAPAP/Mathlib/Combinatorics/Additive/FreimanHom.lean b/LeanAPAP/Mathlib/Combinatorics/Additive/FreimanHom.lean deleted file mode 100644 index ce7f7d0107..0000000000 --- a/LeanAPAP/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Algebra.Group.Submonoid.Operations -import Mathlib.Combinatorics.Additive.FreimanHom - -open Set - -variable {α β S : Type*} [CommMonoid α] [CommMonoid β] [SetLike S α] [SubmonoidClass S α] {n : ℕ} - -@[to_additive] -lemma IsMulFreimanHom.subtypeVal {s : S} : IsMulFreimanHom n (univ : Set s) univ Subtype.val := - MonoidHomClass.isMulFreimanHom (SubmonoidClass.subtype s) (mapsTo_univ ..) diff --git a/LeanAPAP/Mathlib/Data/Finset/Preimage.lean b/LeanAPAP/Mathlib/Data/Finset/Preimage.lean deleted file mode 100644 index 795b742fe3..0000000000 --- a/LeanAPAP/Mathlib/Data/Finset/Preimage.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Mathlib.Data.Finset.Preimage - -namespace Finset -variable {α β : Type*} {f : α → β} {s : Finset β} - -lemma card_preimage (s : Finset β) (f : α → β) (hf) [DecidablePred (· ∈ Set.range f)] : - (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card := - card_nbij f (by simp) (by simpa) (fun b hb ↦ by aesop) - -end Finset diff --git a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean deleted file mode 100644 index 2920eebb80..0000000000 --- a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Mathlib.Data.Fintype.Basic - -attribute [simp] Finset.univ_nonempty diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean deleted file mode 100644 index 189026bf4f..0000000000 --- a/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean +++ /dev/null @@ -1,5 +0,0 @@ -import Mathlib.MeasureTheory.Measure.Count - -open MeasureTheory - -attribute [simp] Measure.count_singleton diff --git a/LeanAPAP/Mathlib/Order/CompleteLattice.lean b/LeanAPAP/Mathlib/Order/CompleteLattice.lean deleted file mode 100644 index 09810ce8d6..0000000000 --- a/LeanAPAP/Mathlib/Order/CompleteLattice.lean +++ /dev/null @@ -1,6 +0,0 @@ -import Mathlib.Order.CompleteLattice - -variable {α : Type*} [CompleteLattice α] - -lemma iSup_le_iSup_of_imp {p q : Prop} {a : α} (h : p → q) : ⨆ _h : p, a ≤ ⨆ _h : q, a := by aesop -lemma iInf_le_iInf_of_imp {p q : Prop} {a : α} (h : p → q) : ⨅ _h : q, a ≤ ⨅ _h : p, a := by aesop diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index b0a33275ed..61f526e7b8 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/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) := diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 26d73ae868..56c1c83f81 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/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, ?_, ?_⟩ diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index cf697e5b8b..061c358e28 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean index 771b865f13..ee4e9b56b4 100644 --- a/LeanAPAP/Prereqs/AddChar/Basic.lean +++ b/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] diff --git a/LeanAPAP/Prereqs/Balance.lean b/LeanAPAP/Prereqs/Balance.lean index 0e59941f8f..e08cb14e38 100644 --- a/LeanAPAP/Prereqs/Balance.lean +++ b/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] diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean index 5e8539e10e..63918bd652 100644 --- a/LeanAPAP/Prereqs/Chang.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index d8ef1f22b6..5d6f9fa26b 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index efde1e2939..1f01d80597 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/PointwiseDensity.lean b/LeanAPAP/Prereqs/PointwiseDensity.lean deleted file mode 100644 index dca272e63f..0000000000 --- a/LeanAPAP/Prereqs/PointwiseDensity.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Mathlib.Algebra.Group.Pointwise.Finset.Basic -import Mathlib.Data.Finset.Density - -open scoped Pointwise - -namespace Finset -variable {α : Type*} [DecidableEq α] [InvolutiveInv α] [Fintype α] - -@[to_additive (attr := simp)] lemma dens_inv (s : Finset α) : s⁻¹.dens = s.dens := by simp [dens] - -end Finset diff --git a/lake-manifest.json b/lake-manifest.json index a9cc34c679..d6e89ffe8b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46", + "rev": "e0b13c946e9c3805f1eec785c72955e103a9cbaf", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "61fb4d1a2a6a4fe4be260ca31c58af1234ff298b", + "rev": "a895713f7701e295a015b1087f3113fd3d615272", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "09c50fb84c0b5e89b270ff20af6ae7e4bd61511e", + "rev": "67904bc4822c8f4dafda24391cfd01f27c23f721", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,