Merge branch 'master' of https://github.com/YaelDillies/LeanAPAP

LeanAPAP.lean

@@ -1,25 +1,23 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Action.Defs
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
+import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
+import LeanAPAP.Mathlib.Algebra.Star.Basic
+import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic
-import LeanAPAP.Mathlib.Data.Rat.Cast.Order
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
+import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC

LeanAPAP/Extras/BSG.lean

@@ -1,5 +1,6 @@
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Data.Real.StarOrdered
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Order
 
 open BigOperators Finset

LeanAPAP/FiniteField/Basic.lean

@@ -1,7 +1,5 @@
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Data.Rat.Cast.Order
+import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Prereqs.Convolution.ThreeAP
-import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.Unbalancing
@@ -229,9 +227,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
           gcongr
           rw [inv_le ‹_› (by positivity)]
           calc
-            65⁻¹ = (1 + 64)⁻¹ := by norm_num
-            _ ≤ log (1 + 64⁻¹) := le_log_one_add_inv (by norm_num)
-            _ = log (65 / 64) := by norm_num
+            65⁻¹ = 1 - (65 / 64)⁻¹ := by norm_num
+            _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)
     _ = ↑(card V) := by simp [card_eq_pow_finrank (K := ZMod q) (V := V)]
     _ ≤ 2 * β⁻¹ ^ 2 := by
       rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,

LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean

@@ -0,0 +1,6 @@
+import Mathlib.Algebra.Group.Action.Defs
+
+@[to_additive]
+lemma smul_mul_smul_comm {α β : Type*} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
+    [IsScalarTower α α β] [SMulCommClass β α β] (a : α) (b : β) (c : α) (d : β) :
+    (a • b) * c • d = (a * c) • (b * d) := smul_smul_smul_comm a b c d

LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean

@@ -0,0 +1,4 @@
+import Mathlib.Algebra.Order.Module.Defs
+
+attribute [gcongr] smul_le_smul_of_nonneg_left smul_le_smul_of_nonneg_right
+  smul_lt_smul_of_pos_left smul_lt_smul_of_pos_right

LeanAPAP/Mathlib/Algebra/Star/Basic.lean

@@ -0,0 +1,12 @@
+import Mathlib.Algebra.Star.Basic
+
+/-!
+# TODO
+
+Swap arguments to `star_nsmul`/`star_zsmul`
+-/
+
+variable {α : Type*}
+
+instance StarAddMonoid.toStarModuleInt [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where
+  star_smul _ _ := star_zsmul _ _

LeanAPAP/Mathlib/Algebra/Star/Rat.lean

@@ -0,0 +1,16 @@
+import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Star.Rat
+
+variable {α : Type*}
+
+@[simp] lemma star_nnqsmul [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] (q : ℚ≥0) (a : α) :
+    star (q • a) = q • star a := sorry
+
+@[simp] lemma star_qsmul [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] (q : ℚ) (a : α) :
+    star (q • a) = q • star a := sorry
+
+instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] :
+    StarModule ℚ≥0 α where star_smul := star_nnqsmul
+
+instance StarAddMonoid.toStarModuleRat [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] :
+    StarModule ℚ α where star_smul := star_qsmul

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

@@ -1,4 +1,6 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import Mathlib.Algebra.EuclideanDomain.Basic
+import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 
 open AddChar Multiplicative Real
 open scoped ComplexConjugate Real

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -1,5 +1,4 @@
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!
 # TODO

LeanAPAP/Mathlib/Data/NNReal/Basic.lean

@@ -1,15 +1,7 @@
 import Mathlib.Data.NNReal.Basic
 
-open Set
-
 namespace NNReal
-variable {ι : Sort*} {f : ι → ℝ≥0}
-
-attribute [simp] coe_sum
 
-@[simp] lemma iSup_eq_zero (hf : BddAbove (range f)) : ⨆ i, f i = 0 ↔ ∀ i, f i = 0 := by
-  cases isEmpty_or_nonempty ι
-  · simp
-  · simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]
+@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ) := rfl
 
 end NNReal

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.EssSup
-import Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory

LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 
 noncomputable section