Yet more nnLpNorm prereqs

LeanAPAP.lean

@@ -1,17 +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.Pow.NNReal
 import LeanAPAP.Mathlib.Data.Fintype.Order
+import LeanAPAP.Mathlib.Data.NNReal.Basic
 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.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/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/Data/NNReal/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib.Data.NNReal.Basic
+
+namespace NNReal
+
+@[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/Probability/ConditionalProbability.lean

@@ -0,0 +1,13 @@
+import Mathlib.Probability.ConditionalProbability
+
+open ENNReal MeasureTheory MeasureTheory.Measure MeasurableSpace Set
+
+variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} (μ : Measure Ω)
+  {s t : Set Ω}
+
+namespace ProbabilityTheory
+
+@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[|s] s = 1 := by
+  simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs
+
+end ProbabilityTheory