linfty_ap

LeanAPAP.lean

@@ -18,6 +18,7 @@ import LeanAPAP.Mathlib.Algebra.Group.TypeTags
 import LeanAPAP.Mathlib.Algebra.ModEq
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Field.Basic
+import LeanAPAP.Mathlib.Algebra.Order.Floor
 import LeanAPAP.Mathlib.Algebra.Order.Group.Abs
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
@@ -26,7 +27,6 @@ import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Algebra.Star.Pi
 import LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
 import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
@@ -90,6 +90,7 @@ import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.AddChar.Circle
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Chang
+import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Cut
 import LeanAPAP.Prereqs.Density
 import LeanAPAP.Prereqs.Discrete.Convolution.Basic
@@ -110,8 +111,8 @@ import LeanAPAP.Prereqs.Indicator
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.MeanInequalities
-import LeanAPAP.Prereqs.Misc
 import LeanAPAP.Prereqs.Multinomial
 import LeanAPAP.Prereqs.Rudin
 import LeanAPAP.Prereqs.SalemSpencer
 import LeanAPAP.Prereqs.Translate
+import LeanAPAP.Prereqs.WideDiag

LeanAPAP/FiniteField/Basic.lean

@@ -1,7 +1,7 @@
 import LeanAPAP.Physics.Unbalancing
 import LeanAPAP.Prereqs.Discrete.Convolution.Norm
 import LeanAPAP.Prereqs.Discrete.DFT.Compact
-import LeanAPAP.Prereqs.Misc
+import LeanAPAP.Prereqs.Curlog
 
 /-!
 # Finite field case
@@ -24,13 +24,14 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
   set p := 2 * ⌈γ.curlog⌉₊
   have hp : 1 < p :=
     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 (by exact_mod_cast hp)
+  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' ℝ)]
   calc
     _ ≤ _ := div_le_div_of_le (card G).cast_nonneg hAC
     _ = |⟪balance (μ A) ∗ balance (μ A), μ C⟫_[ℝ]| := ?_
-    _ ≤ ‖balance (μ_[ℝ] A) ∗ balance (μ A)‖_[p] * ‖μ_[ℝ] C‖_[↑(1 - (p : ℝ≥0)⁻¹ : ℝ≥0)⁻¹] :=
-      (abs_l2Inner_le_lpNorm_mul_lpNorm ⟨by exact_mod_cast hp, ?_⟩ _ _)
+    _ ≤ ‖balance (μ_[ℝ] A) ∗ balance (μ A)‖_[p] * ‖μ_[ℝ] C‖_[NNReal.conjExponent p] :=
+        abs_l2Inner_le_lpNorm_mul_lpNorm hp'' _ _
     _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) :=
         mul_le_mul (lpNorm_conv_le_lpNorm_dconv' (by positivity) (even_two_mul _) _) ?_
           (by positivity) (by positivity)
@@ -40,10 +41,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
   · rw [←balance_conv, balance, l2Inner_sub_left, l2Inner_const_left, expect_conv, sum_mu ℝ hA,
       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 [NNReal.coe_inv, NNReal.coe_sub hp'.le]
-    simp
-  · rw [lpNorm_mu (one_le_inv (tsub_pos_of_lt hp') tsub_le_self) hC, NNReal.coe_inv,
-      NNReal.coe_sub hp'.le, NNReal.coe_one, inv_inv, sub_sub_cancel_left, ←mul_rpow]
+  · rw [lpNorm_mu hp''.symm.one_le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_nat_cast, ←mul_rpow]
     rw [le_div_iff, mul_comm] at hγC
     refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _)
     all_goals positivity
@@ -58,7 +56,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
     rw [←neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos]
     refine' (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $
       inv_le_inv_of_le (curlog_pos hγ hγ₁) $ Nat.le_ceil _).trans $
-        (rpow_neg_inv_curlog hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num
+        (rpow_neg_inv_curlog_le hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num
     all_goals positivity
 
 variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ}

LeanAPAP/Mathlib/Algebra/BigOperators/Basic.lean

@@ -212,18 +212,30 @@ lemma prod_mul_prod_comm (f g h i : α → β) :
     (∏ a in s, f a * g a) * ∏ a in s, h a * i a = (∏ a in s, f a * h a) * ∏ a in s, g a * i a := by
   simp_rw [prod_mul_distrib, mul_mul_mul_comm]
 
+-- TODO: Backport arguments changes to `card_congr` and `prod_bij`
 @[to_additive]
 lemma prod_nbij (i : α → γ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a))
-    (i_inj : ∀ a₁ a₂, a₁ ∈ s → a₂ ∈ s → i a₁ = i a₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ∈ s, b = i a) : ∏ x in s, f x = ∏ x in t, g x :=
-  prod_bij (fun a _ ↦ i a) hi h i_inj $ by simpa using i_surj
+    (i_inj : (s : Set α).InjOn i) (i_surj : (s : Set α).SurjOn i t) :
+    ∏ x in s, f x = ∏ x in t, g x :=
+  prod_bij (fun a _ ↦ i a) hi h (fun a b ha hb ↦ i_inj ha hb) $ by
+    simpa [Set.SurjOn, Set.subset_def, eq_comm] using i_surj
 
 @[to_additive]
 lemma prod_nbij' (i : α → γ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a)) (j : γ → α)
     (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) :
     ∏ x in s, f x = ∏ x in t, g x :=
   prod_bij' (fun a _ ↦ i a) hi h (fun b _ ↦ j b) hj left_inv right_inv
 
+-- TODO: Replace `Finset.Equiv.sum_comp_finset`?
+variable {ι κ α : Type*} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} in
+/-- `Finset.prod_equiv` is a specialization of `Finset.prod_bij` that automatically fills in
+most arguments. -/
+@[to_additive "`Finset.sum_equiv` is a specialization of `Finset.sum_bij` that automatically fills
+in most arguments."]
+lemma prod_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
+    ∏ i ∈ s, f i = ∏ i ∈ t, g i :=
+  prod_nbij e (fun i ↦ (hst _).1) hfg (e.injective.injOn _) fun i hi ↦ ⟨e.symm i, by simpa [hst]⟩
+
 -- TODO: Replace `prod_ite_one`
 @[to_additive]
 lemma prod_ite_one' (s : Finset α) (p : α → Prop) [DecidablePred p]
@@ -248,8 +260,8 @@ lemma prod_union_eq_right (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) :
 lemma prod_diag (s : Finset α) (f : α × α → β) : ∏ i in s.diag, f i = ∏ i in s, f (i, i) :=
   Eq.symm $
     prod_nbij (fun i ↦ (i, i)) (fun _i hi ↦ mem_diag.2 ⟨hi, rfl⟩) (fun _i _ ↦ rfl)
-      (fun _i _j _ _ h ↦ (Prod.ext_iff.1 h).1) fun i hi ↦
-      ⟨i.1, (mem_diag.1 hi).1, Prod.ext rfl (mem_diag.1 hi).2.symm⟩
+      (fun _ _ _ _ h ↦ (Prod.ext_iff.1 h).1) fun i hi ↦
+      ⟨i.1, (mem_diag.1 hi).1, Prod.ext rfl (mem_diag.1 hi).2⟩
 
 end Finset
 

LeanAPAP/Mathlib/Algebra/Order/Floor.lean

@@ -0,0 +1,12 @@
+import Mathlib.Algebra.Order.Floor
+
+section
+variable {α : Type*} [LinearOrderedRing α] [FloorRing α] {a : α}
+
+@[simp] lemma natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋ := by
+  simp [← Nat.cast_floor_eq_int_floor ha]
+
+@[simp] lemma natCast_ceil_eq_intCast_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉ := by
+  simp [← Nat.cast_ceil_eq_int_ceil ha]
+
+end

LeanAPAP/Mathlib/Data/Finset/Basic.lean

@@ -3,6 +3,8 @@ import Mathlib.Data.Finset.Basic
 namespace Finset
 variable {α : Type*} {s : Finset α} {a : α}
 
+attribute [pp_dot] Finset.Nonempty
+
 @[norm_cast]
 lemma coe_subset_singleton : (s : Set α) ⊆ {a} ↔ s ⊆ {a} := by rw [←coe_subset, coe_singleton]
 

LeanAPAP/Mathlib/Data/Real/ConjugateExponents.lean

@@ -6,15 +6,106 @@ import Mathlib.Data.Real.ConjugateExponents
 Change everything to using `x⁻¹` instead of `1 / x`.
 -/
 
+open scoped ENNReal
+
 namespace Real.IsConjugateExponent
 variable {p q : ℝ} (h : p.IsConjugateExponent q)
 
+attribute [mk_iff] IsConjugateExponent
+
 lemma inv_add_inv_conj' : p⁻¹ + q⁻¹ = 1 := by simpa only [one_div] using h.inv_add_inv_conj
 
+lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := sub_eq_of_eq_add' h.inv_add_inv_conj'.symm
+lemma inv_sub_one : p⁻¹ - 1 = -q⁻¹ := by rw [← h.inv_add_inv_conj', sub_add_cancel']
+
 lemma inv_add_inv_conj_nnreal' : p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1 := by
   simpa only [one_div] using h.inv_add_inv_conj_nnreal
 
 lemma inv_add_inv_conj_ennreal' : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1 := by
   simpa only [one_div] using h.inv_add_inv_conj_ennreal
 
 end Real.IsConjugateExponent
+
+namespace NNReal
+
+/-- Two nonnegative real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality
+`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
+norms. -/
+@[mk_iff, pp_dot]
+structure IsConjExponent (p q : ℝ≥0) : Prop where
+  one_lt : 1 < p
+  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
+
+/-- The conjugate exponent of `p` is `q = p/(p-1)`, so that `1/p + 1/q = 1`. -/
+noncomputable def conjExponent (p : ℝ≥0) : ℝ≥0 := p / (p - 1)
+
+variable {a b p q : ℝ≥0} (h : p.IsConjExponent q)
+
+@[simp, norm_cast]
+lemma isConjugateExponent_coe : (p : ℝ).IsConjugateExponent q ↔ p.IsConjExponent q := by
+  simp [Real.IsConjugateExponent_iff, IsConjExponent_iff]; norm_cast
+
+alias ⟨_, IsConjExponent.coe⟩ := isConjugateExponent_coe
+
+lemma isConjExponent_iff (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) := by
+  rw [← isConjugateExponent_coe, Real.isConjugateExponent_iff (mod_cast h), ← NNReal.coe_eq,
+    NNReal.coe_div, NNReal.coe_sub h.le, NNReal.coe_one]
+
+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. -/
+lemma one_le : 1 ≤ p := h.one_lt.le
+lemma pos : 0 < p := zero_lt_one.trans h.one_lt
+lemma ne_zero : p ≠ 0 := h.pos.ne'
+
+lemma sub_one_pos : 0 < p - 1 := tsub_pos_of_lt h.one_lt
+lemma sub_one_ne_zero : p - 1 ≠ 0 := h.sub_one_pos.ne'
+
+lemma inv_pos : 0 < p⁻¹ := _root_.inv_pos.2 h.pos
+lemma inv_ne_zero : p⁻¹ ≠ 0 := h.inv_pos.ne'
+
+lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := tsub_eq_of_eq_add_rev h.inv_add_inv_conj.symm
+
+protected lemma conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
+  (isConjExponent_iff h).2 rfl
+
+lemma conj_eq : q = p / (p - 1) := by
+  simpa only [← NNReal.coe_one, ← NNReal.coe_sub h.one_le, ← NNReal.coe_div, NNReal.coe_eq]
+    using h.coe.conj_eq
+
+-- TODO: Rename `Real` version
+lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
+
+lemma sub_one_mul_conj : (p - 1) * q = p :=
+  mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conj_eq
+
+lemma mul_eq_add : p * q = p + q := by
+  simpa only [← NNReal.coe_mul, ← NNReal.coe_add, NNReal.coe_eq] using h.coe.mul_eq_add
+
+@[symm]
+protected lemma symm : q.IsConjExponent p where
+  one_lt := by
+      rw [h.conj_eq]
+      exact (one_lt_div h.sub_one_pos).mpr (tsub_lt_self h.pos zero_lt_one)
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+
+lemma div_conj_eq_sub_one : p / q = p - 1 := by field_simp [h.symm.ne_zero]; rw [h.sub_one_mul_conj]
+
+lemma inv_add_inv_conj_ennreal : (p⁻¹ + q⁻¹ : ℝ≥0∞) = 1 := by norm_cast; exact h.inv_add_inv_conj
+
+protected lemma inv_inv (ha : a ≠ 0) (hb : b ≠ 0) (hab : a + b = 1) :
+    a⁻¹.IsConjExponent b⁻¹ :=
+  ⟨one_lt_inv ha.bot_lt $ by rw [← hab]; exact lt_add_of_pos_right _ hb.bot_lt, by
+    simpa only [inv_inv] using hab⟩
+
+lemma inv_one_sub_inv (ha₀ : a ≠ 0) (ha₁ : a < 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
+  .inv_inv ha₀ (tsub_pos_of_lt ha₁).ne' $ add_tsub_cancel_of_le ha₁.le
+
+lemma one_sub_inv_inv (ha₀ : a ≠ 0) (ha₁ : a < 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ :=
+  (inv_one_sub_inv ha₀ ha₁).symm
+
+end IsConjExponent
+end NNReal

LeanAPAP/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

@@ -5,7 +5,7 @@ variable {α β : Type*}
 namespace Finset
 variable [Fintype α] [Nonempty α] [ConditionallyCompleteLattice β]
 
-lemma sup'_univ_eq_csupr (f : α → β) : univ.sup' univ_nonempty f = ⨆ i, f i := by
+lemma sup'_univ_eq_ciSup (f : α → β) : univ.sup' univ_nonempty f = ⨆ i, f i := by
   simp [sup'_eq_csSup_image, iSup]
 
 lemma inf'_univ_eq_cinfi (f : α → β) : univ.inf' univ_nonempty f = ⨅ i, f i := by