Skip to content

Commit

Permalink
Bump mathlib
Browse files Browse the repository at this point in the history
YaelDillies committed Aug 26, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 0e6c20d commit 7bc4dcd
Showing 13 changed files with 23 additions and 292 deletions.
1 change: 0 additions & 1 deletion LeanAPAP.lean
Original file line number Diff line number Diff line change
@@ -2,7 +2,6 @@ import LeanAPAP.Extras.BSG
import LeanAPAP.FiniteField.Basic
import LeanAPAP.Mathlib.Algebra.Group.AddChar
import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
import LeanAPAP.Mathlib.Analysis.RCLike.Basic
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
6 changes: 3 additions & 3 deletions LeanAPAP/Extras/BSG.lean
Original file line number Diff line number Diff line change
@@ -286,7 +286,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
refine h.le.trans ?_
rw [mul_assoc]
gcongr _ * ?_
field_simp [hA, hB, hK, le_div_iff, div_le_iff] at hE ⊢
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
· ring_nf
· ring_nf
@@ -407,8 +407,8 @@ theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ)
· rw [← mul_inv, inv_mul_eq_div]
exact oneOfPair_bound (filter_subset _ _) this (hX₃.trans_eq' (by norm_num)) hX₂
have := big_quadruple_bound (H := H) (fun x hx ↦ (mem_filter.1 hx).2) (filter_subset _ _) hX₂
rw [le_div_iff (by positivity)]
rw [mul_div_assoc', div_le_iff (by positivity)] at this
rw [le_div_iff (by positivity)]
rw [mul_div_assoc', div_le_iff (by positivity)] at this
exact this.trans_eq (by ring)

theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) :
14 changes: 6 additions & 8 deletions LeanAPAP/FiniteField/Basic.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
import LeanAPAP.Mathlib.Data.Rat.Cast.Order
import LeanAPAP.Prereqs.Convolution.ThreeAP
import LeanAPAP.Prereqs.FourierTransform.Compact
@@ -30,7 +28,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ hγ₁)
have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp
have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp
rw [mul_comm, ← div_div, div_le_iff (zero_lt_two' ℝ)]
rw [mul_comm, ← div_div, div_le_iff (zero_lt_two' ℝ)]
calc
_ ≤ _ := div_le_div_of_nonneg_right hAC (card G).cast_nonneg
_ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_
@@ -46,7 +44,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
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 [nnratCast_dens, le_div_iff, mul_comm] at hγC
rw [nnratCast_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]
@@ -128,7 +126,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
-- mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)]
· have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry
sorry
-- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity),
-- simpa [wlpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity),
-- ← div_div, *] using global_dichotomy hA hγC hγ hAC
sorry

@@ -148,7 +146,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
have : 0 < log q := log_pos ‹_›
obtain hα | hα := le_total (q ^ (n / 2) : ℝ) (2 * α⁻¹ ^ 2)
· rw [rpow_le_iff_le_log, log_mul, log_pow, Nat.cast_two, ← mul_div_right_comm,
mul_div_assoc, ← le_div_iff] at hα
mul_div_assoc, ← le_div_iff] at hα
calc
_ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα
_ = 4 / log q * (log α⁻¹ + log 2 / 2) := by ring
@@ -213,7 +211,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
all_goals positivity
rw [hB.l2Inner_mu_conv_mu_mu_two_smul_mu] at hBV
suffices h : (q ^ (n - 65 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) by
rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff' zero_lt_two, ← mul_assoc] at h
rw [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff' zero_lt_two, ← mul_assoc] at h
norm_num at h
exact h
calc
@@ -239,7 +237,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,
← div_eq_mul_inv (card V : ℝ), ← zpow_one_sub_natCast₀ (by positivity)] at hBV
have : 0 < (card V : ℝ) := by positivity
simpa [le_inv_mul_iff₀', mul_inv_le_iff₀', this, zero_lt_two, mul_comm] using hBV
simpa [le_inv_mul_iff₀, mul_inv_le_iff₀, this, zero_lt_two, mul_comm] using hBV
_ ≤ 2 * α⁻¹ ^ 2 := by gcongr
_ ≤ _ := hα
simpa [card_eq_pow_finrank (K := ZMod q) (V := V), ZMod.card] using hq'.pow
235 changes: 0 additions & 235 deletions LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

This file was deleted.

1 change: 0 additions & 1 deletion LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled

namespace Real
variable {x : ℝ}
30 changes: 0 additions & 30 deletions LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Original file line number Diff line number Diff line change
@@ -3,36 +3,6 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real
namespace Real
variable {x y z : ℝ}

lemma rpow_le_iff_le_log (hx : 0 < x) (hy : 0 < y) : x ^ z ≤ y ↔ z * log x ≤ log y := by
rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

lemma rpow_lt_iff_lt_log (hx : 0 < x) (hy : 0 < y) : x ^ z < y ↔ z * log x < log y := by
rw [← log_lt_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

lemma pow_le_iff_le_log {n : ℕ} (hx : 0 < x) (hy : 0 < y) :
x ^ n ≤ y ↔ n * log x ≤ log y := by rw [← rpow_le_iff_le_log hx hy, rpow_natCast]

lemma zpow_le_iff_le_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) :
x ^ n ≤ y ↔ n * log x ≤ log y := by rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

lemma pow_lt_iff_lt_log {n : ℕ} (hx : 0 < x) (hy : 0 < y) :
x ^ n < y ↔ n * log x < log y := by rw [← rpow_lt_iff_lt_log hx hy, rpow_natCast]

lemma zpow_lt_iff_lt_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) :
x ^ n < y ↔ n * log x < log y := by rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast]

lemma le_pow_iff_log_le {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ log x ≤ n * log y := by
rw [← le_rpow_iff_log_le hx hy, rpow_natCast]

lemma le_zpow_iff_log_le {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ log x ≤ n * log y := by
rw [← le_rpow_iff_log_le hx hy, rpow_intCast]

lemma lt_pow_iff_log_lt {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ log x < n * log y := by
rw [← lt_rpow_iff_log_lt hx hy, rpow_natCast]

lemma lt_zpow_iff_log_lt {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ log x < n * log y := by
rw [← lt_rpow_iff_log_lt hx hy, rpow_intCast]

-- TODO: Replace in mathlib
alias rpow_add_intCast := rpow_add_int
alias rpow_add_natCast := rpow_add_nat
6 changes: 3 additions & 3 deletions LeanAPAP/Physics/AlmostPeriodicity.lean
Original file line number Diff line number Diff line change
@@ -110,8 +110,8 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hk : 64 * m / ε ^ 2 ≤ k) :
refine pow_le_pow_left (by positivity) ?_ _
rw [mul_right_comm, mul_comm _ ε, mul_pow, ← mul_assoc, sq (k : ℝ), ← mul_assoc]
refine mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg k)
rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff' (zero_lt_two' ℝ),
← div_le_iff', ← mul_assoc]
rw [mul_right_comm, div_mul_eq_mul_div, one_mul, div_mul_eq_mul_div, le_div_iff' (zero_lt_two' ℝ),
← div_le_iff', ← mul_assoc]
· norm_num1; exact hk
positivity

@@ -337,7 +337,7 @@ lemma T_bound (hK' : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ) *
have : (0 : ℝ) < Ac ^ k := by positivity
refine le_of_mul_le_mul_left ?_ this
have : (Ac : ℝ) ^ k ≤ K * Lc := by
rw [div_le_iff'] at h₂
rw [div_le_iff'] at h₂
refine h₂.trans (mul_le_mul_of_nonneg_right hK' (Nat.cast_nonneg _))
exact zero_lt_two
rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm,
8 changes: 4 additions & 4 deletions LeanAPAP/Physics/DRC.lean
Original file line number Diff line number Diff line change
@@ -101,7 +101,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂
positivity
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]
rw [div_mul_div_comm, le_div_iff]
simpa [hg_def, hM_def, mul_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
mul_div_right_comm] using h
positivity
@@ -188,11 +188,11 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
_ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
_ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by
simp [l2Inner_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
_ ≤ _ := (le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h
_ ≤ _ := (le_div_iff $ lpNorm_conv_pos hp₀.ne' hB hA).2 h
_ ≤ _ := ?_
· simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu]
rw [sum_mu _ hA₁, sum_mu _ hA₂, one_mul]
rw [div_le_iff (lpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff' (zero_lt_two' ℝ)]
rw [div_le_iff (lpNorm_conv_pos hp₀.ne' hB hA), ← le_div_iff' (zero_lt_two' ℝ)]
simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole,
sum_ite_mem, univ_inter, mul_div_right_comm]
calc
@@ -236,7 +236,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even 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 [nnratCast_dens, le_div_iff, ← mul_div_right_comm]
rw [nnratCast_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]
2 changes: 1 addition & 1 deletion LeanAPAP/Physics/Unbalancing.lean
Original file line number Diff line number Diff line change
@@ -144,7 +144,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
set p' := 24 / ε * log (3 / ε) * p
have hp' : 0 < p' := p'_pos hp hε₀ hε₁
have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by
rw [← div_le_iff, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this
rw [← div_le_iff, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this
calc
_ ≤ exp (-(8⁻¹ * ε)) := one_sub_le_exp_neg _
_ = ((ε / 3) ^ p * (ε / 3) ^ (2 * p)) ^ p'⁻¹ := ?_
4 changes: 2 additions & 2 deletions LeanAPAP/Prereqs/Chang.lean
Original file line number Diff line number Diff line change
@@ -76,7 +76,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x
sum_mul_sq_le_sq_mul_sq _ _ _
_ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ in Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by
simp_rw [l2Norm_sq_eq_sum, mul_pow, sq_sqrt (NNReal.coe_nonneg _), pow_right_comm]; rfl
rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff',
rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff',
mul_div_assoc, mul_div_assoc] at this
calc
_ ≤ _ := this
@@ -100,7 +100,7 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0)
↑Δ.card ^ (2 * m) * (η ^ (2 * m) * α f) ≤ boringEnergy m Δ := by
have hG : (0 : ℝ) < card G := by positivity
simpa [boringEnergy, α, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc,
div_le_iff hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using
div_le_iff hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using
general_hoelder hη 1 (fun (_ : G) _ ↦ le_rfl) hΔ hm

noncomputable def changConst : ℝ := 32 * exp 1
2 changes: 1 addition & 1 deletion LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
Original file line number Diff line number Diff line change
@@ -226,7 +226,7 @@ theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a
_ ≤ (4 * ↑(m + 1)) ^ (m + 1) * n ^ m * ∑ a in A ^^ n, ∑ i, f (a i) ^ (2 * (m + 1)) := by
simp_rw [mul_assoc, mul_sum]; rfl
gcongr with a
rw [← div_le_iff']
rw [← div_le_iff']
have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) univ m fun i _ ↦ ?_
simpa only [Finset.card_fin, pow_mul] using this
all_goals { positivity }
2 changes: 1 addition & 1 deletion LeanAPAP/Prereqs/Rudin.lean
Original file line number Diff line number Diff line change
@@ -114,7 +114,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
_ = (2 * exp 2⁻¹) ^ p := by
rw [hfp, sq_sqrt, mul_pow, ← exp_nsmul, nsmul_eq_mul, div_eq_mul_inv]; positivity
refine le_of_pow_le_pow_left hp₀ (by positivity) ?_
rwa [hfp, mul_assoc, mul_self_sqrt, mul_pow, ← div_le_iff, ← div_pow]
rwa [hfp, mul_assoc, mul_self_sqrt, mul_pow, ← div_le_iff, ← div_pow]
all_goals positivity

/-- **Rudin's inequality**, usual form. -/
4 changes: 2 additions & 2 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
"rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@@ -65,7 +65,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "9b07fb6d08b58de5b55813b29f5ac9aa6fa0b1ad",
"rev": "b5f7e1c26c6cb2be97c2ad36bf7038c159e359b3",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,

0 comments on commit 7bc4dcd

Please sign in to comment.