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

L2PullbackRange: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Exact range of real L2 pullback
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.