invariant_kernel_l2_operator

Plain-English statement

- A finite invariant Markov kernel induces a real L2 contraction realizing its genuine conditional integrals. It preserves order, one and the mean; detailed balance additionally makes it self-adjoint. No topology or nonempty premise is required. See the sealed statement for all representative and AE quantifiers.

Lean statement

theorem invariant_kernel_l2_operator {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ] (hκ : κ.Invariant μ) :
    invariant_kernel_l2_statement μ κ hκ := by
  classical
  obtain ⟨A, hA, hpair⟩ := pair_operator μ κ hκ
  let ν := μ ⊗ₘ κ
  have hfst : MeasurePreserving Prod.fst ν μ :=
    ⟨measurable_fst, Measure.fst_compProd μ κ⟩
  have hsnd : MeasurePreserving Prod.snd ν μ :=
    ⟨measurable_snd, (Measure.snd_compProd μ κ).trans hκ.def⟩
  have hrep : ∀ G : X → ℝ, ∀ hG : MemLp G 2 μ,
      (∀ᵐ x ∂μ, Integrable G (κ x)) ∧
      (A (hG.toLp G) : X → ℝ) =ᵐ[μ] fun x => ∫ z, G z ∂κ x := by
    intro G hG
    have hprod : Integrable (fun p : X × X => G p.2) ν :=
      (hG.comp_measurePreserving hsnd).integrable (by norm_num)
    have hc : Integrable G ((κ ∘ₖ Kernel.const Unit μ) ()) := by
      simpa only [Kernel.comp_const, Kernel.const_apply, hκ.def] using
        hG.integrable (by norm_num)
    have hop : Integrable (fun x => ∫ z, G z ∂κ x) μ := by
      simpa only [Kernel.const_apply] using hc.integral_comp
    have hAg : Integrable (A (hG.toLp G) : X → ℝ) μ :=
      (Lp.memLp _).integrable (by norm_num)
    refine ⟨Measure.ae_integrable_of_integrable_comp (by
      simpa only [hκ.def] using hG.integrable (by norm_num)), ?_⟩
    apply Integrable.ae_eq_of_forall_setIntegral_eq _ _ hAg hop
    intro s hs hms
    let i : Lp ℝ 2 μ := indicatorConstLp 2 hs hms.ne (1 : ℝ)
    have hi : (i : X → ℝ) =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) :=
      indicatorConstLp_coeFn
    have hi' := hfst.quasiMeasurePreserving.ae_eq hi
    have hg' := hsnd.quasiMeasurePreserving.ae_eq hG.coeFn_toLp
    let F : X × X → ℝ := fun p => s.indicator (fun _ => (1 : ℝ)) p.1 * G p.2
    have hF : Integrable F ν := by
      have he : F = (Prod.fst ⁻¹' s).indicator (fun p : X × X => G p.2) := by
        funext p
        by_cases hp : p.1 ∈ s <;> simp [F, Set.indicator, hp]
      rw [he]
      exact hprod.indicator (hs.preimage measurable_fst)
    calc
      (∫ x in s, A (hG.toLp G) x ∂μ) = ⟪i, A (hG.toLp G)⟫_ℝ :=
        (L2.inner_indicatorConstLp_one hs hms.ne _).symm
      _ = ∫ p : X × X, i p.1 * (hG.toLp G) p.2 ∂ν := hpair i (hG.toLp G)
      _ = ∫ p, F p ∂ν := by
        apply integral_congr_ae
        filter_upwards [hi', hg'] with p hp hq
        change i p.1 = s.indicator (fun _ => (1 : ℝ)) p.1 at hp
        change (hG.toLp G) p.2 = G p.2 at hq
        simp only [F, hp, hq]
      _ = ∫ x, ∫ z, F (x, z) ∂κ x ∂μ := Measure.integral_compProd hF
      _ = ∫ x, s.indicator (fun _ => (1 : ℝ)) x * (∫ z, G z ∂κ x) ∂μ := by
        simp only [F, integral_const_mul]
      _ = ∫ x in s, (∫ z, G z ∂κ x) ∂μ := by
        rw [← integral_indicator hs]
        congr 1
        funext x
        by_cases hx : x ∈ s <;> simp [Set.indicator, hx]
  have hrepLp (f : Lp ℝ 2 μ) :
      (A f : X → ℝ) =ᵐ[μ] fun x => ∫ z, f z ∂κ x := by
    simpa only [Lp.toLp_coeFn] using (hrep f (Lp.memLp f)).2
  refine ⟨A, hA, hrep, ?_, ?_, ?_, ?_⟩
  · intro f hf
    have hp : ∀ᵐ x ∂μ, ∀ᵐ z ∂κ x, 0 ≤ f z :=
      Measure.ae_ae_of_ae_comp (by simpa only [hκ.def] using hf)
    filter_upwards [hrepLp f, hp] with x hx hp
    rw [hx]
    exact integral_nonneg_of_ae hp
  · have hc := (hrep (fun _ : X => (1 : ℝ)) (memLp_const (1 : ℝ))).2
    rw [MemLp.toLp_const] at hc
    apply Lp.ext
    filter_upwards [hc, Lp.coeFn_const (p := 2) (μ := μ) (c := (1 : ℝ))] with x hx h1
    calc
      A (Lp.const 2 μ (1 : ℝ)) x = 1 := by simpa [measureReal_def] using hx
      _ = Lp.const 2 μ (1 : ℝ) x := h1.symm
  · intro f
    have hprod : Integrable (fun p : X × X => f p.2) ν :=
      ((Lp.memLp f).comp_measurePreserving hsnd).integrable (by norm_num)
    calc
      (∫ x, A f x ∂μ) = ∫ x, ∫ z, f z ∂κ x ∂μ := integral_congr_ae (hrepLp f)
      _ = ∫ p : X × X, f p.2 ∂ν := (Measure.integral_compProd hprod).symm
      _ = ∫ x, f x ∂ν.map Prod.snd :=
        (integral_map_of_stronglyMeasurable measurable_snd (Lp.stronglyMeasurable f)).symm
      _ = ∫ x, f x ∂μ := by rw [hsnd.map_eq]
  · intro hrev
    have hswap : ν.map Prod.swap = ν := by
      apply Measure.ext_prod
      intro s t hs ht
      rw [Measure.map_apply measurable_swap (hs.prod ht)]
      have he : Prod.swap ⁻¹' (s ×ˢ t) = t ×ˢ s := by ext p; simp [and_comm]
      rw [he, Measure.compProd_apply_prod ht hs, Measure.compProd_apply_prod hs ht]
      exact hrev ht hs
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro f g
    calc
      ⟪A f, g⟫_ℝ = ⟪g, A f⟫_ℝ := real_inner_comm _ _
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν := hpair g f
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν.map Prod.swap := by rw [hswap]
      _ = ∫ p : X × X, g p.2 * f p.1 ∂ν := by
        have hm : StronglyMeasurable (fun p : X × X => g p.1 * f p.2) :=
          ((Lp.stronglyMeasurable g).comp_measurable measurable_fst).mul
            ((Lp.stronglyMeasurable f).comp_measurable measurable_snd)
        exact integral_map_of_stronglyMeasurable measurable_swap hm
      _ = ∫ p : X × X, f p.1 * g p.2 ∂ν := by simp only [mul_comm]
      _ = ⟪f, A g⟫_ℝ := (hpair f g).symm

end
end AutoSamplingTheory.TechnicalLemmas.Probability.KernelL2

Open AutoSamplingTheory/TechnicalLemmas/Probability/KernelL2.lean:82published source at ed709a7f320d

Proof architecture

Planned actual retained-coordinate half-turn A.2/A.9 and one-step observable B.1 adapters; no SALD completion

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `intro` introduces quantified hypotheses into the local proof context.
• `have` creates a named intermediate mathematical fact.
• `calc` records an equality or inequality chain matching a paper calculation.
• `rw` rewrites by an established identity.
• `simp` normalizes through registered definitional and theorem rewrites.
• `apply` reduces the goal to the hypotheses of a reusable theorem.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.
• Integrability is an input or proved output; a displayed integral alone does not supply it.
• Almost-everywhere hypotheses depend on the stated measure and representative.
• Density statements retain normalization and absolute-continuity prerequisites.