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

Actual PBPS macroscopic range and centering

Attributed ASTIS mathematical completion/consumer of Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang PBPS AppendixB macro identification and centered C3-C4. Generic factorization background is ASTIS-authored via fixed Mathlib; not claimed as verbatim source.

PBPS2609.06905v1;Lean4.33.0/fixedMathlib · 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. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J). For the canonical isometric pullback M u(x,y)=u(y), both J and ν are probabilities, ran M=ran P, and ∫Mu dJ=∫u dν for every u∈L²(ν). Consequently M maps the full zero-mean subspace of L²(ν) onto exactly {f∈ran P:∫f dJ=0}. No caller onto, centering, probability or law certificate is assumed.

  • Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J).
  • Centering and macro range restrict the conclusion input; no supplied operator/law/onto/root certificate.
  • Base finite dimension does not imply finite-dimensional L2; rank zero is explicitly extended.

Actual PBPS macroscopic range and centering

\[\operatorname{ran}M=\operatorname{ran}P,\quad\int Mu\,dJ=\int u\,d\nu,\quad M(L^2_0(\nu))=\operatorname{ran}P\cap L^2_0(J).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual PBPS macroscopic range and centering

AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange.actual_macroscopic_centered_range · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J). For the canonical isometric pullback M u(x,y)=u(y), both J and ν are probabilities, ran M=ran P, and ∫Mu dJ=∫u dν for every u∈L²(ν). Consequently M maps the full zero-mean subspace of L²(ν) onto exactly {f∈ran P:∫f dJ=0}. No caller onto, centering, probability or law certificate is assumed.

\[\operatorname{ran}M=\operatorname{ran}P,\quad\int Mu\,dJ=\int u\,d\nu,\quad M(L^2_0(\nu))=\operatorname{ran}P\cap L^2_0(J).\]
Lean statement · actual_macroscopic_centered_range

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J). For the canonical isometric pullback M u(x,y)=u(y), both J and ν are probabilities, ran M=ran P, and ∫Mu dJ=∫u dν for every u∈L²(ν). Consequently M maps the full zero-mean subspace of L²(ν) onto exactly {f∈ran P:∫f dJ=0}. No caller onto, centering, probability or law certificate is assumed.

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 actual_macroscopic_centered_range
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let hp : MeasurePreserving (Prod.snd : E × E → E) J ν :=
      ⟨measurable_snd,rfl⟩
    let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J :=
      Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      (lpMeas ℝ ℝ (MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E))
        2 J).subtypeL ∘L condExpL2 ℝ ℝ measurable_snd.comap_le
    IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
      M.toLinearMap.range = P.toLinearMap.range ∧
      (∀ u : Lp ℝ 2 ν, (∫ p, (M u) p ∂J) = ∫ y, u y ∂ν) ∧
      M '' {u : Lp ℝ 2 ν | (∫ y, u y ∂ν)=0} =
        {f : Lp ℝ 2 J | f ∈ P.toLinearMap.range ∧ (∫ p, f p ∂J)=0}

Exact module and namespace context

Proof roadmap

  1. 1Produce the actual probabilities

    The existing normalized Gibbs augmentation theorem under the original lower curvature and positive η produces probability μ and J internally. The true second marginal ν is therefore probability; no normalization certificate is a premise.

  2. 2Identify both ranges with the same closed subspace

    Apply the shared exact pullback-range theorem to the actual measure-preserving second projection. The actual conditional expectation is definitionally the Hilbert orthogonal projection onto that same lpMeas submodule, whose range equals the submodule.

  3. 3Transport the actual mean

    The canonical pullback agrees AE with u∘snd. Integration against the true pushforward ν=J.snd gives ∫Mu dJ=∫u dν. L2 functions are L1 here because J and ν are probabilities; no injectivity or embedding of snd is assumed.

  4. 4Obtain the full centered image

    Forward range membership and mean transport send every centered u to a centered macro class. Conversely, every centered f in ranP lies in ranM; choosing its actual preimage and applying mean transport proves that preimage centered. Thus the equality is onto the entire centered macro subspace.

Full assumptions and notation

All objects and hypotheses

  • Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J).
  • Centering and macro range restrict the conclusion input; no supplied operator/law/onto/root certificate.
  • Base finite dimension does not imply finite-dimensional L2; rank zero is explicitly extended.

Mathematical proof

1. Produce the actual probabilities

The existing normalized Gibbs augmentation theorem under the original lower curvature and positive η produces probability μ and J internally. The true second marginal ν is therefore probability; no normalization certificate is a premise.

\[J=\operatorname{Law}(X,X+\sqrt\eta Z),\quad J(E\times E)=\nu(E)=1.\]
Corresponding Lean step

GibbsAugmentation.normalized_augmentation_density; hJ; hν

2. Identify both ranges with the same closed subspace

Apply the shared exact pullback-range theorem to the actual measure-preserving second projection. The actual conditional expectation is definitionally the Hilbert orthogonal projection onto that same lpMeas submodule, whose range equals the submodule.

\[\operatorname{ran}M=L^2(\sigma(Y),J)=\operatorname{ran}P.\]
Corresponding Lean step

L2PullbackRange.l2_pullback_range_eq_lpMeas; hPdef; S.range_starProjection; hRange

3. Transport the actual mean

The canonical pullback agrees AE with u∘snd. Integration against the true pushforward ν=J.snd gives ∫Mu dJ=∫u dν. L2 functions are L1 here because J and ν are probabilities; no injectivity or embedding of snd is assumed.

\[\int Mu\,dJ=\int u(Y)\,dJ=\int u\,d\nu.\]
Corresponding Lean step

Lp.coeFn_compMeasurePreserving; integral_congr_ae; integral_map; hMean

4. Obtain the full centered image

Forward range membership and mean transport send every centered u to a centered macro class. Conversely, every centered f in ranP lies in ranM; choosing its actual preimage and applying mean transport proves that preimage centered. Thus the equality is onto the entire centered macro subspace.

\[M(L^2_0(\nu))=\{f\in\operatorname{ran}P:\int f\,dJ=0\}.\]
Corresponding Lean step

hRange; hMean; ext f; centered-image forward/reverse proof

Lean verification

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

Lean proof · actual_macroscopic_centered_range

Produce the actual probabilities; Identify both ranges with the same closed subspace; Transport the actual mean; Obtain the full centered image

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 actual_macroscopic_centered_range
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    let hp : MeasurePreserving (Prod.snd : E × E → E) J ν :=
      ⟨measurable_snd,rfl⟩
    let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J :=
      Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
    let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
      (lpMeas ℝ ℝ (MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E))
        2 J).subtypeL ∘L condExpL2 ℝ ℝ measurable_snd.comap_le
    IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
      M.toLinearMap.range = P.toLinearMap.range ∧
      (∀ u : Lp ℝ 2 ν, (∫ p, (M u) p ∂J) = ∫ y, u y ∂ν) ∧
      M '' {u : Lp ℝ 2 ν | (∫ y, u y ∂ν)=0} =
        {f : Lp ℝ 2 J | f ∈ P.toLinearMap.range ∧ (∫ p, f p ∂J)=0} := by
  classical
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
  let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
  let S := lpMeas ℝ ℝ (MeasurableSpace.comap Prod.snd
    (inferInstance : MeasurableSpace E)) 2 J
  let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J :=
    S.subtypeL ∘L condExpL2 ℝ ℝ measurable_snd.comap_le
  obtain ⟨_,hJ,_⟩ := GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x v => (hH x v).1) hη
  letI : IsProbabilityMeasure J := hJ
  have hν : IsProbabilityMeasure ν := by infer_instance
  letI : IsProbabilityMeasure ν := hν
  letI : Fact ((MeasurableSpace.comap Prod.snd
    (inferInstance : MeasurableSpace E)) ≤ (inferInstance : MeasurableSpace (E × E))) :=
    ⟨measurable_snd.comap_le⟩
  have hMrange : M.toLinearMap.range = S :=
    AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange.l2_pullback_range_eq_lpMeas hp
  have hPdef : P = S.starProjection := rfl
  have hPrange : P.toLinearMap.range = S := by
    change P.range = S
    rw [hPdef]
    exact S.range_starProjection
  have hRange : M.toLinearMap.range = P.toLinearMap.range := hMrange.trans hPrange.symm
  have hMean (u : Lp ℝ 2 ν) : (∫ p, (M u) p ∂J) = ∫ y, u y ∂ν := by
    calc
      (∫ p, (M u) p ∂J) = ∫ p : E × E, u p.2 ∂J :=
        integral_congr_ae (Lp.coeFn_compMeasurePreserving u hp)
      _ = ∫ y, u y ∂ν :=
        (integral_map measurable_snd.aemeasurable (Lp.aestronglyMeasurable u)).symm
  refine ⟨hJ,hν,hRange,hMean,?_⟩
  ext f
  constructor
  · rintro ⟨u,hu,rfl⟩
    refine ⟨?_,?_⟩
    · rw [← hRange]
      exact ⟨u,rfl⟩
    · rw [hMean]
      exact hu
  · rintro ⟨hf,hfmean⟩
    have hfM : f ∈ M.toLinearMap.range := by rwa [hRange]
    obtain ⟨u,hu⟩ := hfM
    refine ⟨u,?_,hu⟩
    change M u=f at hu
    change (∫ y, u y ∂ν)=0
    rw [← hMean u,hu]
    exact hfmean

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Euclidean source standing C2/two global Hessian/capped η and actual macro projection.Finite real Hilbert/Borel/rank0 extension disclosed; real actual L2, canonical pullback and conditional projection.sameOriginal paper hypotheses retained on actual main/Test; generic shared background is independently generalized and used internally.
Macro scalar identification and centered subspace; sharp centered contraction.Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero as an explicit extension of the source Euclidean setting. Let V:E→ℝ be C2, 0<α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Set μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), ν=J.snd. Let P be the actual conditional-expectation orthogonal projection onto the second-coordinate sigma algebra in L²(J). For the canonical isometric pullback M u(x,y)=u(y), both J and ν are probabilities, ran M=ran P, and ∫Mu dJ=∫u dν for every u∈L²(ν). Consequently M maps the full zero-mean subspace of L²(ν) onto exactly {f∈ran P:∫f dJ=0}. No caller onto, centering, probability or law certificate is assumed.sameActual AE factorization/pushforward and same-law Test transport explicitly close the scoped range gap; no added theorem inputs.
Γ/inverse/fullH1/dynamics/main/errors/cost/composition.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.unresolvedSquared defect conclusion is not an operator-root or main theorem.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Finite realHilbert/Borel wording generalizes sourceEuclidean notation;rank0 explicitlydisclosed and no dimension-onL2 assumption. — Independent source classification domain-clarification; native nonblocking result runs/20261007-companion-priority/pbps-macroscopic-centered-range58/source-review58/source.1.review.json preserved.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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)

  • Submodule.range_starProjection
  • integral_map
  • integral_congr_ae
  • Lp.coeFn_compMeasurePreserving

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.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual PBPS macroscopic range and centering
  • TODO — not closed by these contributions Gamma/root/inverse/fullH1/dynamics/main/errors/cost/composition open