Actual PBPS macroscopic range and centering
AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange.actual_macroscopic_centered_range · theorem · Teaching coverage
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.
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.
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}Proof roadmap
- 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.
- 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.
- 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.
- 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.
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.
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.
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.
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.
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.MacroscopicRangeScope 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
AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange.l2_pullback_range_eq_lpMeasAutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation.normalized_augmentation_density
Mathlib API called (external library)
- Submodule.range_starProjection
- integral_map
- integral_congr_ae
- Lp.coeFn_compMeasurePreserving
Mathematical sources
- 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. — 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.