Bump mathlib

LeanAPAP.lean

@@ -4,11 +4,8 @@ import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-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.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
@@ -22,7 +19,6 @@ import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Balance.Complex
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -35,7 +31,6 @@ import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
 import LeanAPAP.Prereqs.Energy
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete

LeanAPAP/Mathlib/Data/Real/ConjExponents.lean

@@ -1,6 +1,5 @@
 import Mathlib.Data.ENNReal.Inv
 import Mathlib.Data.Real.ConjExponents
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 
 open scoped NNReal
 
@@ -20,21 +19,45 @@ variable {a b p q : ℝ≥0∞} (h : p.IsConjExponent q)
 
 @[simp, norm_cast] lemma isConjExponent_coe {p q : ℝ≥0} :
     IsConjExponent p q ↔ p.IsConjExponent q := by
-  simp [NNReal.isConjExponent_iff, isConjExponent_iff]; sorry
+  simp only [isConjExponent_iff, NNReal.isConjExponent_iff]
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
+  · simpa using (ENNReal.lt_add_right (fun hp ↦ by simp [hp] at h) <| by simp).trans_eq h
+  · rw [← coe_inv, ← coe_inv] at h
+    norm_cast at h
+    all_goals rintro rfl; simp at h
+  · rintro ⟨hp, h⟩
+    rw [← coe_inv (zero_lt_one.trans hp).ne', ← coe_inv, ← coe_add, h, coe_one]
+    rintro rfl
+    simp [hp.ne'] at h
 
 alias ⟨_, _root_.NNReal.IsConjExponent.coe_ennreal⟩ := isConjExponent_coe
 
 namespace IsConjExponent
 
-/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
-`q`: many computations using these exponents require clearing out denominators, which can be done
-with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
-ones. -/
+protected lemma conjExponent (hp : 1 ≤ p) : p.IsConjExponent (conjExponent p) := by
+  have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
+  rw [isConjExponent_iff, conjExponent, add_comm]
+  refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (sorry) (by simpa)).1 ?_
+  rw [inv_eq_iff_eq_inv]
+  obtain rfl | hp₁ := hp.eq_or_lt
+  · simp
+  obtain rfl | hp := eq_or_ne p ∞
+  · sorry
+  calc
+    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
+      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
+    _ = (1 - p⁻¹)⁻¹ := by
+      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
+        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]
 
 section
 include h
 
-lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 $ by
+@[symm]
+protected lemma symm : q.IsConjExponent p where
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+
+lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 <| by
   rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]; gcongr; positivity
 
 lemma pos : 0 < p := zero_lt_one.trans_le h.one_le
@@ -43,17 +66,29 @@ lemma ne_zero : p ≠ 0 := h.pos.ne'
 lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ :=
   ENNReal.sub_eq_of_eq_add_rev' one_ne_top h.inv_add_inv_conj.symm
 
-lemma conj_eq : q = 1 + (p - 1)⁻¹ := sorry
-
-lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
-
-lemma mul_eq_add : p * q = p + q := sorry
-
-@[symm]
-protected lemma symm : q.IsConjExponent p where
-  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
-
-lemma div_conj_eq_sub_one : p / q = p - 1 := sorry
+lemma conjExponent_eq : conjExponent p = q := by
+  have hp : 1 ≤ p := h.one_le
+  have : p⁻¹ ≠ ∞ := by simpa using h.ne_zero
+  simpa [ENNReal.add_right_inj, *] using
+    (IsConjExponent.conjExponent hp).inv_add_inv_conj.trans h.inv_add_inv_conj.symm
+
+lemma conj_eq : q = 1 + (p - 1)⁻¹ := h.conjExponent_eq.symm
+
+lemma mul_eq_add : p * q = p + q := by
+  obtain rfl | hp := eq_or_ne p ∞
+  · simp [h.symm.ne_zero]
+  obtain rfl | hq := eq_or_ne q ∞
+  · simp [h.ne_zero]
+  rw [← mul_one (_ * _), ← h.inv_add_inv_conj, mul_add, mul_right_comm,
+    ENNReal.mul_inv_cancel h.ne_zero hp, one_mul, mul_assoc,
+    ENNReal.mul_inv_cancel h.symm.ne_zero hq, mul_one, add_comm]
+
+lemma div_conj_eq_sub_one : p / q = p - 1 := by
+  obtain rfl | hq := eq_or_ne q ∞
+  · sorry
+  refine ENNReal.eq_sub_of_add_eq one_ne_top ?_
+  rw [← ENNReal.div_self h.symm.ne_zero hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
+    ENNReal.div_self h.symm.ne_zero hq, mul_one]
 
 end
 
@@ -65,15 +100,12 @@ lemma inv_one_sub_inv (ha : a ≤ 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
 
 lemma one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ := (inv_one_sub_inv ha).symm
 
-lemma top_one : IsConjExponent ∞ 1 := sorry
-lemma one_top : IsConjExponent 1 ∞ := sorry
+lemma top_one : IsConjExponent ∞ 1 := ⟨by simp⟩
+lemma one_top : IsConjExponent 1 ∞ := ⟨by simp⟩
 
 end IsConjExponent
 
-lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
-  sorry
-
-protected lemma IsConjExponent.conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
-  (isConjExponent_iff_eq_conjExponent h).2 rfl
+lemma isConjExponent_iff_eq_conjExponent (hp : 1 ≤ p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
+  ⟨fun h ↦ h.conj_eq, by rintro rfl; exact .conjExponent hp⟩
 
 end ENNReal

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 

LeanAPAP/Physics/DRC.lean

@@ -87,7 +87,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   set M : ℝ :=
     2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
       with hM_def
-  have hM : 0 < M := by rw [hM_def]; sorry -- positivity
+  have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
     have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f :=
       mul_nonneg (mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg) $ pow_nonneg

LeanAPAP/Prereqs/Balance/Complex.lean

@@ -1,8 +1,9 @@
-import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
+import Mathlib.Algebra.BigOperators.Balance
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 
-open Finset
-open scoped BigOperators NNReal
+open Fintype
+open scoped NNReal
 
 namespace Complex
 variable {ι : Type*}
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -116,9 +116,11 @@ lemma mem_chordSet_iff_norm_width : x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.
 @[simp, norm_cast] lemma coeSort_coe (B : BohrSet G) : ↥(B : Set G) = B := rfl
 
 @[simp] lemma zero_mem : 0 ∈ B.chordSet := by simp [mem_chordSet_iff_nnnorm_width]
+
+-- TODO: This lemma needs `Finite G` because we are using `AddChar G ℂ` rather than `AddChar G ℂˣ`
+-- as the dual group.
 @[simp] lemma neg_mem [Finite G] : -x ∈ B.chordSet ↔ x ∈ B.chordSet :=
-  forall₂_congr fun ψ hψ ↦ by sorry
-    -- rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
+  forall₂_congr fun ψ hψ ↦ by rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
 
 /-! ### Lattice structure -/
 

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -1,6 +1,5 @@
-import LeanAPAP.Prereqs.Balance.Defs
+import Mathlib.Algebra.BigOperators.Balance
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
@@ -393,11 +392,11 @@ end Field
 namespace RCLike
 variable {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G)
 
-@[simp, norm_cast]
-lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_cconv (algebraMap ℝ 𝕜) _ _ _
+@[simp, norm_cast] lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a :=
+  map_cconv (algebraMap ℝ 𝕜) ..
 
-@[simp, norm_cast]
-lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by simp [cdconv_apply, coe_expect]
+@[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by
+  simp [cdconv_apply, ofReal_expect]
 
 @[simp]
 lemma coe_comp_cconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cconv _ _

LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean

@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Balance
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 

LeanAPAP/Prereqs/Energy.lean

@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 

LeanAPAP/Prereqs/FourierTransform/Compact.lean

@@ -11,8 +11,7 @@ Parseval-Plancherel identity and Fourier inversion formula for it.
 
 noncomputable section
 
-open AddChar Finset Function MeasureTheory RCLike
-open Fintype (card)
+open AddChar Finset Fintype Function MeasureTheory RCLike
 open scoped ComplexConjugate ComplexOrder
 
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}