Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Exact range of real L2 pullback

AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange.l2_pullback_range_eq_lpMeas · theorem · Teaching coverage

Read this first

Mathematical statement

Let X,Y be arbitrary measurable spaces, μ,ν arbitrary measures and f:X→Y measure preserving (measurable and f₊μ=ν). Let M_f:L²(ν;ℝ)→L²(μ;ℝ) be canonical isometric pullback. Then its range is exactly the submodule of L²(μ;ℝ) classes having an AE strongly measurable representative for the comap sigma algebra f⁻¹ΣY. There is no probability, finite-measure, standard-Borel or finite-dimensional hypothesis.

\[\operatorname{ran}M_f=L^2(f^{-1}\Sigma_Y,\mu;\mathbb R),\quad M_fu=u\circ f.\]
Lean statement · l2_pullback_range_eq_lpMeas

Let X,Y be arbitrary measurable spaces, μ,ν arbitrary measures and f:X→Y measure preserving (measurable and f₊μ=ν). Let M_f:L²(ν;ℝ)→L²(μ;ℝ) be canonical isometric pullback. Then its range is exactly the submodule of L²(μ;ℝ) classes having an AE strongly measurable representative for the comap sigma algebra f⁻¹ΣY. There is no probability, finite-measure, standard-Borel or finite-dimensional hypothesis.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem l2_pullback_range_eq_lpMeas
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {μ : Measure X} {ν : Measure Y} {f : X → Y}
    (hf : MeasurePreserving f μ ν) :
    (Lp.compMeasurePreservingₗᵢ ℝ f hf).toLinearMap.range =
      lpMeas ℝ ℝ (MeasurableSpace.comap f (inferInstance : MeasurableSpace Y)) 2 μ

Exact module and namespace context

Proof roadmap

  1. 1Pullback has the right measurable representative

    A marginal L2 class has a strongly measurable representative. Composition along the measurable measure-preserving map is AE strongly measurable for its comap sigma algebra; the canonical pullback representative agrees AE with that composition.

  2. 2Factor a genuine reverse representative

    For v in the comap-measurable L2 submodule, choose its genuine AE strongly measurable mk representative. Real-valued measurable factorization yields a measurable g on Y with mk(v)=g∘f. This theorem uses completeness of the real codomain, not a standard-Borel assumption on Y.

  3. 3Push square integrability to the target

    AE equality gives MemLp(g∘f,2,μ). The actual pushforward equality transfers this to MemLp(g,2,ν). The resulting target L2 class pulls back to v by AE equality, proving the reverse range.

Full assumptions and notation

All objects and hypotheses

  • Let X,Y be arbitrary measurable spaces, μ,ν arbitrary measures and f:X→Y measure preserving (measurable and f₊μ=ν). Let M_f:L²(ν;ℝ)→L²(μ;ℝ) be canonical isometric pullback.

Mathematical proof

1. Pullback has the right measurable representative

A marginal L2 class has a strongly measurable representative. Composition along the measurable measure-preserving map is AE strongly measurable for its comap sigma algebra; the canonical pullback representative agrees AE with that composition.

\[[M_fu]=[u\circ f]\in L^2(f^{-1}\Sigma_Y,\mu).\]
Corresponding Lean step

Lp.aestronglyMeasurable; comp_ae_measurable'; Lp.coeFn_compMeasurePreserving; mem_lpMeas_iff_aestronglyMeasurable

2. Factor a genuine reverse representative

For v in the comap-measurable L2 submodule, choose its genuine AE strongly measurable mk representative. Real-valued measurable factorization yields a measurable g on Y with mk(v)=g∘f. This theorem uses completeness of the real codomain, not a standard-Borel assumption on Y.

\[v= g\circ f\quad\mu\text{-a.e.},\qquad g:Y\to\mathbb R\ \text{measurable}.\]
Corresponding Lean step

AEStronglyMeasurable.stronglyMeasurable_mk; StronglyMeasurable.exists_eq_measurable_comp; hvg

3. Push square integrability to the target

AE equality gives MemLp(g∘f,2,μ). The actual pushforward equality transfers this to MemLp(g,2,ν). The resulting target L2 class pulls back to v by AE equality, proving the reverse range.

\[\int|g|^2\,d\nu=\int|g\circ f|^2\,d\mu<\infty,\quad M_f[g]=v.\]
Corresponding Lean step

memLp_map_measure_iff; hf.map_eq; hgLp.toLp; ae_eq_comp; Lp.ext

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · l2_pullback_range_eq_lpMeas

Pullback has the right measurable representative; Factor a genuine reverse representative; Push square integrability to the target

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem l2_pullback_range_eq_lpMeas
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {μ : Measure X} {ν : Measure Y} {f : X → Y}
    (hf : MeasurePreserving f μ ν) :
    (Lp.compMeasurePreservingₗᵢ ℝ f hf).toLinearMap.range =
      lpMeas ℝ ℝ (MeasurableSpace.comap f (inferInstance : MeasurableSpace Y)) 2 μ := by
  classical
  ext v
  constructor
  · rintro ⟨u, rfl⟩
    apply mem_lpMeas_iff_aestronglyMeasurable.mpr
    have hu : AEStronglyMeasurable (u : Y → ℝ) (μ.map f) := by
      rw [hf.map_eq]
      exact Lp.aestronglyMeasurable u
    exact (hu.comp_ae_measurable' hf.aemeasurable).congr
      (Lp.coeFn_compMeasurePreserving u hf).symm
  · intro hv
    have hm := mem_lpMeas_iff_aestronglyMeasurable.mp hv
    obtain ⟨g, hg, heq⟩ := hm.stronglyMeasurable_mk.exists_eq_measurable_comp
    have hvg : (v : X → ℝ) =ᵐ[μ] g ∘ f :=
      hm.ae_eq_mk.trans (Filter.Eventually.of_forall (fun x => congrFun heq x))
    have hcomp : MemLp (g ∘ f) 2 μ := (Lp.memLp v).ae_eq hvg
    have hgLp : MemLp g 2 ν := by
      rw [← hf.map_eq]
      exact (memLp_map_measure_iff hg.aestronglyMeasurable hf.aemeasurable).mpr hcomp
    have hgAE : (hgLp.toLp g : Y → ℝ) =ᵐ[μ.map f] g := by
      rw [hf.map_eq]
      exact hgLp.coeFn_toLp
    refine ⟨hgLp.toLp g, ?_⟩
    apply Lp.ext
    exact (Lp.coeFn_compMeasurePreserving (hgLp.toLp g) hf).trans
      ((ae_eq_comp hf.aemeasurable hgAE).trans hvg.symm)

end
end AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange

Exact module and namespace context

Scope and omitted-condition boundaries
  • PBPS2609.06905v1 AppendixB B1-B5 exact macro identification/centering feeding C3-C4 and B15. Public actual canonical pullback range=P range and centered image equality; real new Test transports exact57 scalar contraction to all actual centered macro f and squared defect gap. Finite real Hilbert/Borel/rank0 explicit extension; trueL2 generally infinite dimensional. Public generic pullback range and actual PBPS range/mean/centered image; realTest-only allmacro contraction/squaredBgap. NoGamma/fullweakH1/B13/B14/dynamics/main/cost/composition/fullpaper/Goal claim.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • StronglyMeasurable.exists_eq_measurable_comp
    • AEStronglyMeasurable.comp_ae_measurable'
    • memLp_map_measure_iff
    • Lp.coeFn_compMeasurePreserving
    • Lp.ext

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.