Bump mathlib

LeanAPAP.lean

@@ -5,7 +5,6 @@ import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
-import LeanAPAP.Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
@@ -14,7 +13,6 @@ import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
@@ -39,18 +37,20 @@ import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Function.Translate
+import LeanAPAP.Prereqs.Inner.Compact.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact.Defs
-import LeanAPAP.Prereqs.LpNorm.Compact.Inner
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm

LeanAPAP/FiniteField/Basic.lean

@@ -1,12 +1,11 @@
 import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
-import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
-import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
+import LeanAPAP.Prereqs.Function.Indicator.Complex
 
 /-!
 # Finite field case

LeanAPAP/Mathlib/Algebra/Group/AddChar.lean

@@ -1,17 +1,9 @@
 import Mathlib.Algebra.Group.AddChar
 
-open Finset hiding card
-open Fintype (card)
-open Function
-open scoped NNRat
-
-variable {G H R : Type*}
+variable {G R : Type*}
 
 namespace AddChar
-section AddMonoid
-variable [AddMonoid G] [AddMonoid H] [CommMonoid R] {ψ : AddChar G R}
-
-instance instAddCommMonoid : AddCommMonoid (AddChar G R) := Additive.addCommMonoid
+variable [AddMonoid G] [CommMonoid R] {ψ : AddChar G R}
 
 @[simp] lemma toMonoidHomEquiv_zero : toMonoidHomEquiv (0 : AddChar G R) = 1 := rfl
 @[simp] lemma toMonoidHomEquiv_symm_one :
@@ -22,98 +14,8 @@ instance instAddCommMonoid : AddCommMonoid (AddChar G R) := Additive.addCommMono
 @[simp] lemma toMonoidHomEquiv_symm_mul (ψ φ : Multiplicative G →* R) :
   toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ := rfl
 
-lemma eq_zero_iff : ψ = 0 ↔ ∀ x, ψ x = 1 := DFunLike.ext_iff
-lemma ne_zero_iff : ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
-
-@[simp, norm_cast] lemma coe_zero : ⇑(0 : AddChar G R) = 1 := rfl
-
-lemma zero_apply (a : G) : (0 : AddChar G R) a = 1 := rfl
-
-@[simp, norm_cast] lemma coe_eq_zero : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]
-@[simp, norm_cast] lemma coe_add (ψ χ : AddChar G R) : ⇑(ψ + χ) = ψ * χ := rfl
-
-lemma add_apply (ψ χ : AddChar G R) (a : G) : (ψ + χ) a = ψ a * χ a := rfl
-
-@[simp, norm_cast] lemma coe_nsmul (n : ℕ) (ψ : AddChar G R) : ⇑(n • ψ) = ψ ^ n := rfl
-
-lemma nsmul_apply (n : ℕ) (ψ : AddChar G R) (a : G) : (ψ ^ n) a = ψ a ^ n := rfl
-
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma coe_sum (s : Finset ι) (ψ : ι → AddChar G R) : ∑ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
-  induction s using Finset.cons_induction <;> simp [*]
-
-lemma sum_apply (s : Finset ι) (ψ : ι → AddChar G R) (a : G) :
-    (∑ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_sum, Finset.prod_apply]
+@[simp, norm_cast] lemma coe_eq_one : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]
 
 noncomputable instance : DecidableEq (AddChar G R) := Classical.decEq _
 
-/-- The double dual embedding. -/
-def doubleDualEmb : G →+ AddChar (AddChar G R) R where
-  toFun a := { toFun := fun ψ ↦ ψ a
-               map_zero_eq_one' := by simp
-               map_add_eq_mul' := by simp }
-  map_zero' := by ext; simp
-  map_add' _ _ := by ext; simp [map_add_eq_mul]
-
-@[simp] lemma doubleDualEmb_apply (a : G) (ψ : AddChar G R) : doubleDualEmb a ψ = ψ a := rfl
-
-end AddMonoid
-
-section AddGroup
-variable [AddGroup G]
-
-section CommSemiring
-variable [Fintype G] [CommSemiring R] [IsDomain R] {ψ : AddChar G R}
-
-lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) else 0 := by
-  split_ifs with h
-  · simp [h, card_univ]
-  obtain ⟨x, hx⟩ := ne_one_iff.1 h
-  refine eq_zero_of_mul_eq_self_left hx ?_
-  rw [Finset.mul_sum]
-  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
-
-variable [CharZero R]
-
-lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
-  rw [sum_eq_ite, Ne.ite_eq_right_iff]
-  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-
-lemma sum_ne_zero_iff_eq_zero : ∑ x, ψ x ≠ 0 ↔ ψ = 0 :=
-  sum_eq_zero_iff_ne_zero.not_left
-
-end CommSemiring
-end AddGroup
-
-section AddCommGroup
-variable [AddCommGroup G]
-
-section CommMonoid
-variable [CommMonoid R]
-
-/-- The additive characters on a commutative additive group form a commutative group. -/
-instance : AddCommGroup (AddChar G R) :=
-  @Additive.addCommGroup (AddChar G R) _
-
-@[simp]
-lemma neg_apply (ψ : AddChar G R) (a : G) : (-ψ) a = ψ (-a) := rfl
-
-@[simp]
-lemma sub_apply (ψ χ : AddChar G R) (a : G) : (ψ - χ) a = ψ a * χ (-a) := rfl
-
-end CommMonoid
-
-section DivisionCommMonoid
-variable [DivisionCommMonoid R]
-
-lemma neg_apply' (ψ : AddChar G R) (x : G) : (-ψ) x = (ψ x)⁻¹ :=
-  map_neg_eq_inv _ _
-
-lemma sub_apply' (ψ χ : AddChar G R) (a : G) : (ψ - χ) a = ψ a / χ a := by
-  rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
-
-end DivisionCommMonoid
-end AddCommGroup
 end AddChar

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -523,4 +523,3 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
     _ = ε := by simp only [sum_const, card_fin, nsmul_eq_mul]; rw [mul_div_cancel₀]; positivity
 
 end AlmostPeriodicity
-#min_imports

LeanAPAP/Physics/Unbalancing.lean

@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -1,6 +1,6 @@
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Prereqs.Expect.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 open Finset hiding card
 open Fintype (card)

LeanAPAP/Prereqs/Bohr/Arc.lean

@@ -1,6 +1,5 @@
 import Mathlib.Analysis.Complex.Angle
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Bohr.Basic
 
 /- ### Arc Bohr sets -/

LeanAPAP/Prereqs/Convolution/Norm.lean

@@ -1,7 +1,7 @@
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # Norm of a convolution

LeanAPAP/Prereqs/Convolution/ThreeAP.lean

@@ -2,7 +2,7 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # The convolution characterisation of 3AP-free sets

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -1,11 +1,12 @@
+import Mathlib.Algebra.Algebra.Rat
+import Mathlib.Algebra.BigOperators.GroupWithZero.Action
 import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.Module.Rat
-import Mathlib.Algebra.Algebra.Field
-import Mathlib.Algebra.Star.Order
-import Mathlib.Analysis.CStarAlgebra.Basic
-import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
-import Mathlib.Data.Real.Sqrt
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Data.Finset.Density
+import Mathlib.Data.Finset.Pointwise.Basic
+import Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset
@@ -25,7 +26,7 @@ This file defines `Finset.expect`, the average (aka expectation) of a function o
 
 open Function
 open Fintype (card)
-open scoped Pointwise NNRat NNReal
+open scoped Pointwise NNRat
 
 variable {ι κ α β : Type*}
 
@@ -218,13 +219,14 @@ lemma card_smul_expect (s : Finset ι) (f : ι → α) : s.card • 𝔼 i ∈ s
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
-    positivity
+    exact mod_cast hs.card_ne_zero
 
 @[simp] nonrec lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → α) :
     Fintype.card ι • 𝔼 i, f i = ∑ i, f i := card_smul_expect _ _
 
 @[simp] lemma expect_const (hs : s.Nonempty) (a : α) : 𝔼 _i ∈ s, a = a := by
-  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]; positivity
+  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
+  exact mod_cast hs.card_ne_zero
 
 lemma smul_expect {G : Type*} [DistribSMul G α] [SMulCommClass G ℚ≥0 α] (a : G)
     (s : Finset ι) (f : ι → α) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by
@@ -360,11 +362,11 @@ lemma _root_.GCongr.expect_le_expect (h : ∀ i ∈ s, f i ≤ g i) : s.expect f
   Finset.expect_le_expect h
 
 lemma expect_le (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a :=
-  (inv_smul_le_iff_of_pos $ by positivity).2 $ by
+  (inv_smul_le_iff_of_pos $ mod_cast hs.card_pos).2 $ by
     rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h
 
 lemma le_expect (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, a ≤ f x) : a ≤ 𝔼 i ∈ s, f i :=
-  (le_inv_smul_iff_of_pos $ by positivity).2 $ by
+  (le_inv_smul_iff_of_pos $ mod_cast hs.card_pos).2 $ by
     rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h
 
 lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i :=
@@ -394,7 +396,7 @@ section PosSMulStrictMono
 variable [PosSMulStrictMono ℚ≥0 α]
 
 lemma expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i :=
-  smul_pos (by positivity) $ sum_pos hf hs
+  smul_pos (inv_pos.2 $ mod_cast hs.card_pos) $ sum_pos hf hs
 
 end PosSMulStrictMono
 end OrderedCancelAddCommMonoid
@@ -493,49 +495,3 @@ 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)
-
-namespace Mathlib.Meta.Positivity
-open Qq Lean Meta
-
-@[positivity Finset.expect _ _]
-def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
-  match e with
-  | ~q(@Finset.expect $ι _ $instα $instmod $s $f) =>
-    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
-    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
-      try
-        let _fi ← synthInstanceQ q(Fintype $ι)
-        let _no ← synthInstanceQ q(Nonempty $ι)
-        match s with
-        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
-        | _ => pure none
-      catch _ => do
-        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-        pure (some (.fvar fv))
-    match ← core zα pα rhs, so with
-    | .nonnegative pb, _ => do
-      let instαordmon ← synthInstanceQ q(OrderedAddCommMonoid $α)
-      let instαordsmul ← synthInstanceQ q(PosSMulMono ℚ≥0 $α)
-      assumeInstancesCommute
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
-      return .nonnegative q(@expect_nonneg $ι $α $instαordmon $instmod $s $f $instαordsmul
-        fun i _ ↦ $pr i)
-    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-      let instαordmon ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
-      let instαordsmul ← synthInstanceQ q(PosSMulStrictMono ℚ≥0 $α)
-      assumeInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
-      return .positive q(@expect_pos $ι $α $instαordmon $instmod $s $f $instαordsmul
-        (fun i _ ↦ $pr i) $fi)
-    | _, _ => pure .none
-  | _ => throwError "not Finset.expect"
-
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
-example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity
-example (a : ℕ → ℝ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by
-  have : Finset.Nonempty {1} := singleton_nonempty 1
-  positivity
-
-end Mathlib.Meta.Positivity