IsProper.integral_mul WIP

GibbsMeasure.lean

@@ -4,14 +4,18 @@ import GibbsMeasure.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import GibbsMeasure.Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
 import GibbsMeasure.Mathlib.MeasureTheory.Function.L1Space.Integrable
 import GibbsMeasure.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import GibbsMeasure.Mathlib.MeasureTheory.Function.SimpleFunc
+import GibbsMeasure.Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
+import GibbsMeasure.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
 import GibbsMeasure.Mathlib.MeasureTheory.Integral.Bochner.Basic
 import GibbsMeasure.Mathlib.MeasureTheory.MeasurableSpace.Basic
+import GibbsMeasure.Mathlib.MeasureTheory.Measure.AEMeasurable
 import GibbsMeasure.Mathlib.MeasureTheory.Measure.GiryMonad
 import GibbsMeasure.Mathlib.MeasureTheory.Measure.Prod
 import GibbsMeasure.Mathlib.Probability.Kernel.Condexp
+import GibbsMeasure.Mathlib.Probability.Kernel.Proper
 import GibbsMeasure.Prereqs.Filtration.Consistent
 import GibbsMeasure.Prereqs.Juxt
 import GibbsMeasure.Prereqs.Kernel.CondExp
-import GibbsMeasure.Prereqs.Kernel.Proper
 import GibbsMeasure.Prereqs.LebesgueCondExp
 import GibbsMeasure.Specification

GibbsMeasure/Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

@@ -1,10 +1,10 @@
+import GibbsMeasure.Mathlib.MeasureTheory.Measure.AEMeasurable
 import Mathlib.MeasureTheory.Function.L1Space.Integrable
 
-open EMetric ENNReal Filter MeasureTheory NNReal Set
+open EMetric ENNReal Filter MeasureTheory NNReal TopologicalSpace Set
 
-variable {α β γ δ ε 𝕜 : Type*} {m : MeasurableSpace α} {μ ν : Measure α} [MeasurableSpace δ]
-variable [NormedAddCommGroup β] [NormedAddCommGroup γ] [ENorm ε] {𝕜 : Type*} [NormedField 𝕜]
-  [NormedSpace 𝕜 β] {f φ : α → 𝕜}
+variable {α β 𝕜 : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α}
+variable [NormedField 𝕜] {f φ : α → 𝕜}
 
 namespace MeasureTheory
 
@@ -15,4 +15,9 @@ namespace MeasureTheory
     Integrable (fun x ↦ φ x * f x) μ :=
   hφ.smul_of_top_left hf
 
+@[fun_prop]
+lemma Integrable.measurable [TopologicalSpace β] [PseudoMetrizableSpace β] [ContinuousENorm β]
+    [μ.IsComplete] {f : α → β} [BorelSpace β] (hf : Integrable f μ) : Measurable f :=
+  hf.aemeasurable.measurable
+
 end MeasureTheory

GibbsMeasure/Mathlib/MeasureTheory/Function/SimpleFunc.lean

@@ -0,0 +1,9 @@
+import Mathlib.MeasureTheory.Function.SimpleFunc
+
+namespace MeasureTheory.SimpleFunc
+variable {α β : Type*}
+
+scoped infixr:25 " →ₛ " => SimpleFunc
+scoped notation:25 α:26 " →ₛ[" mα "] " β:25 => @SimpleFunc α mα β
+
+end MeasureTheory.SimpleFunc

GibbsMeasure/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

@@ -0,0 +1,21 @@
+import Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
+import Mathlib.MeasureTheory.Integral.IntegrableOn
+
+open ENNReal Function
+
+namespace MeasureTheory
+variable {α E : Type*} {mα : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α}
+
+-- TODO: Replace in mathlib
+@[elab_as_elim]
+lemma Integrable.induction' (P : ∀ f : α → E, Integrable f μ → Prop)
+    (indicator : ∀ c s (hs : MeasurableSet s) (hμs : μ s ≠ ∞),
+      P (s.indicator fun _ ↦ c) ((integrable_indicator_iff hs).2 integrableOn_const))
+    (add : ∀ (f g : α → E) (hf : Integrable f μ) (hg : Integrable g μ),
+        Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) (hf.add hg))
+    (isClosed : IsClosed {f : α →₁[μ] E | P f (L1.integrable_coeFn f)})
+    (ae_congr : ∀ (f g) (hf : Integrable f μ) (hfg : f =ᵐ[μ] g), P f hf → P g (hf.congr hfg)) :
+    ∀ (f : α → E) (hf : Integrable f μ), P f hf := by
+  sorry
+
+end MeasureTheory

GibbsMeasure/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+
+namespace MeasureTheory
+
+attribute [fun_prop] StronglyMeasurable.indicator stronglyMeasurable_one
+
+end MeasureTheory

GibbsMeasure/Mathlib/MeasureTheory/Measure/AEMeasurable.lean

@@ -0,0 +1,3 @@
+import Mathlib.MeasureTheory.Measure.AEMeasurable
+
+alias ⟨AEMeasurable.measurable, _⟩ := aemeasurable_iff_measurable

GibbsMeasure/Mathlib/Probability/Kernel/Proper.lean

@@ -0,0 +1,83 @@
+import GibbsMeasure.Mathlib.Data.ENNReal.Basic
+import GibbsMeasure.Mathlib.MeasureTheory.Function.SimpleFunc
+import GibbsMeasure.Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
+import GibbsMeasure.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+import GibbsMeasure.Mathlib.MeasureTheory.Integral.Bochner.Basic
+import GibbsMeasure.Mathlib.MeasureTheory.MeasurableSpace.Basic
+import Mathlib.MeasureTheory.Integral.DominatedConvergence
+import Mathlib.Probability.Kernel.Proper
+
+/-!
+# Proper kernels
+
+We define the notion of properness for measure kernels and highlight important consequences.
+-/
+
+open MeasureTheory ENNReal NNReal Set
+open scoped ProbabilityTheory
+
+namespace ProbabilityTheory.Kernel
+variable {X : Type*} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel[𝓑, 𝓧] X X} {A B : Set X}
+  {f g : X → ℝ} {x₀ : X}
+
+private lemma IsProper.integral_indicator_mul_indicator (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hπ : IsProper π)
+    (hA : MeasurableSet[𝓧] A) (hB : MeasurableSet[𝓑] B) :
+    ∫ x, (B.indicator 1 x * A.indicator 1 x : ℝ) ∂(π x₀) =
+      B.indicator 1 x₀ * ∫ x, A.indicator 1 x ∂(π x₀) := by
+  calc
+        ∫ x, (B.indicator 1 x * A.indicator 1 x : ℝ) ∂(π x₀)
+    _ = (∫⁻ x, .ofReal (B.indicator 1 x * A.indicator 1 x) ∂π x₀).toReal :=
+      integral_eq_lintegral_of_nonneg_ae (.of_forall <| by simp [indicator_nonneg, mul_nonneg])
+        (by measurability)
+    _ = (∫⁻ x, B.indicator 1 x * A.indicator 1 x ∂π x₀).toReal := by
+      simp [ofReal_mul, indicator_nonneg]
+    _ = (B.indicator 1 x₀ * ∫⁻ x, A.indicator 1 x ∂π x₀).toReal := by
+      rw [hπ.lintegral_mul h𝓑𝓧 (by measurability) (by measurability)]
+    _ = B.indicator 1 x₀ * ∫ x, A.indicator 1 x ∂π x₀ := by
+      rw [integral_eq_lintegral_of_nonneg_ae (.of_forall <| by simp [indicator_nonneg, mul_nonneg])
+        (by measurability)]
+      simp [ofReal_mul]
+
+open scoped SimpleFunc in
+private lemma IsProper.integral_simpleFunc_mul_indicator (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hπ : IsProper π)
+    (hA : MeasurableSet[𝓧] A) (g : X →ₛ[𝓑] ℝ) :
+    ∫ x, g x * A.indicator 1 x ∂(π x₀) = g x₀ * ∫ x, A.indicator 1 x ∂(π x₀) := sorry
+
+variable [IsFiniteKernel π]
+
+private lemma IsProper.integral_bdd_mul_indicator (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hπ : IsProper π)
+    (hA : MeasurableSet[𝓧] A) (hg : StronglyMeasurable[𝓑] g) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C)
+    (x₀ : X) :
+    ∫ x, g x * A.indicator 1 x ∂(π x₀) = g x₀ * ∫ x, A.indicator 1 x ∂(π x₀) := by
+  obtain ⟨C, hC⟩ := hgbdd
+  refine tendsto_nhds_unique ?_ <| (hg.tendsto_approxBounded_of_norm_le <| hC _).mul_const _
+  simp_rw [← hπ.integral_simpleFunc_mul_indicator h𝓑𝓧 hA]
+  refine tendsto_integral_of_dominated_convergence (fun _ ↦ C) (fun n ↦ ?_) (integrable_const _)
+    (fun n ↦ .of_forall fun x ↦ ?_) <| .of_forall fun x ↦ ?_
+  · exact (((hg.approxBounded C n).stronglyMeasurable.mono h𝓑𝓧).mul
+      (by fun_prop (disch := assumption))).aestronglyMeasurable
+  · simpa [-norm_mul] using
+      norm_mul_le_of_le (hg.norm_approxBounded_le ((norm_nonneg _).trans <| hC x₀) _ _)
+        (norm_indicator_le_norm_self 1 _)
+  · exact .mul_const _ <| hg.tendsto_approxBounded_of_norm_le <| hC _
+
+lemma IsProper.integral_bdd_mul (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hπ : IsProper π)
+    (hf : Integrable[𝓧] f (π x₀)) (hg : StronglyMeasurable[𝓑] g) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) :
+    ∫ x, g x * f x ∂(π x₀) = g x₀ * ∫ x, f x ∂(π x₀) := by
+  induction f, hf using Integrable.induction' with
+  | indicator c s hs _ =>
+    simp [← smul_indicator_one_apply, mul_left_comm, integral_const_mul,
+      hπ.integral_bdd_mul_indicator h𝓑𝓧 hs hg hgbdd]
+  | add f₁ f₂ hf₁ hf₂ _ hgf₁ hgf₂ =>
+    have : Integrable (fun x ↦ g x * f₁ x) (π x₀) :=
+      hf₁.bdd_mul (hg.mono h𝓑𝓧).aestronglyMeasurable hgbdd
+    have : Integrable (fun x ↦ g x * f₂ x) (π x₀) :=
+      hf₂.bdd_mul (hg.mono h𝓑𝓧).aestronglyMeasurable hgbdd
+    simp [mul_add, integral_add, *]
+  | isClosed =>
+    refine isClosed_eq ?_ <| by fun_prop
+    sorry
+  | ae_congr f₁ f₂ hf₁ hf hgf₁ =>
+    simpa [integral_congr_ae <| .mul .rfl hf, integral_congr_ae hf] using hgf₁
+
+end ProbabilityTheory.Kernel