The actual PBPS conditional mean on all of L2
AutoSamplingTheory.ExampleCases.ProximalBPS.L2MacroscopicMean.actual_macroscopic_l2_mean · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2 and 0<α≤β, with α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), ν=J.snd, Λ=J.map((x,y)↦(y,2x−y)), F(x,y)=(x,2x−y), and P the actual L2 conditional orthogonal projection onto the snd-comap measurable subspace. Then μ,J,ν are probabilities; one measurable Markov kernel S has EVERY-y identity S_y=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), disintegrates Λ, and Λ.fst=Λ.snd=ν. There are an actual J-reflection isometric involution/self-adjoint U, one linear isometry M:L²(ν)→L²(J) representing the snd pullback AE J, and one bounded linear T:L²(ν)→L²(ν), all chosen before every rough u∈L²(ν). With A=PUP and B=(1−P)UP, PMu=Mu, MTu=AMu, ‖Tu‖≤‖u‖, and Tu(y)=∫u(x)S_y(dx) AE ν. For AE y both u and u² are integrable under S_y; the centered source variance is integrable under ν and ∫Var(S_y,u)ν(dy)=‖BMu‖²=‖u‖²−‖Tu‖². No centering, compactness, caller law/kernel/operator/coherence/normalizer certificate, or pointwise rough regularity is assumed. This is attributed background integration for B.1/B.9, not the full rough gradient B.13 or a main sampling theorem.
Lean statement · actual_macroscopic_l2_mean
Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2 and 0<α≤β, with α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v. Let η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), ν=J.snd, Λ=J.map((x,y)↦(y,2x−y)), F(x,y)=(x,2x−y), and P the actual L2 conditional orthogonal projection onto the snd-comap measurable subspace. Then μ,J,ν are probabilities; one measurable Markov kernel S has EVERY-y identity S_y=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)), disintegrates Λ, and Λ.fst=Λ.snd=ν. There are an actual J-reflection isometric involution/self-adjoint U, one linear isometry M:L²(ν)→L²(J) representing the snd pullback AE J, and one bounded linear T:L²(ν)→L²(ν), all chosen before every rough u∈L²(ν). With A=PUP and B=(1−P)UP, PMu=Mu, MTu=AMu, ‖Tu‖≤‖u‖, and Tu(y)=∫u(x)S_y(dx) AE ν. For AE y both u and u² are integrable under S_y; the centered source variance is integrable under ν and ∫Var(S_y,u)ν(dy)=‖BMu‖²=‖u‖²−‖Tu‖². No centering, compactness, caller law/kernel/operator/coherence/normalizer certificate, or pointwise rough regularity is assumed. This is attributed background integration for B.1/B.9, not the full rough gradient B.13 or a main sampling theorem.
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_l2_mean
{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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
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 μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
∃ S : Kernel E E, IsMarkovKernel S ∧
(∀ y, S y = (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
∃ M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ u : Lp ℝ 2 ν, (M u : E × E → ℝ) =ᵐ[J] u ∘ Prod.snd) ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
let A := P * U.toContinuousLinearMap * P
let B := (1-P) * U.toContinuousLinearMap * P
∀ u : Lp ℝ 2 ν,
P (M u) = M u ∧ M (T u) = A (M u) ∧ ‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∀ᵐ y ∂ν, Integrable (u : E → ℝ) (S y) ∧
Integrable (fun x => (u x)^2) (S y)) ∧
Integrable (fun y =>
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
(S y) (u : E → ℝ)) ν ∧
(∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
(S y) (u : E → ℝ) ∂ν) = ‖B (M u)‖^2 ∧
‖B (M u)‖^2 = ‖u‖^2-‖T u‖^2Proof roadmap
- 1Use the same laws and the actual second-coordinate pullback
The existing macroscopic-energy theorem supplies μ,J,ν probability and genuine S,U,P on the exact source laws, including literal every-y S identity and compact-observer coherence. Since ν=J.snd, snd is measure preserving from J to ν. Mathlib constructs its canonical linear isometry M and the AE pullback representative. This is an actual map between full L2 spaces, not a finite-dimensional Lp assumption.
- 2Pass the true compact coherence to all L2 inputs
The existing actual Gaussian-marginal gradient core has dense smoothcompact domain. For its compact representative f, the real macroscopic parent supplies g=f∘snd, Pg=g and Ag=(Tf)∘snd, with Tf genuinely L2. Canonical AE uniqueness gives Mu=g and AMu=M[Tf]. The isometry has closed range because L2 is complete. PM=M is a closed equality and AMu∈rangeM a closed preimage; density extends both properties to every u.
- 3Construct one bounded operator by the closed-range inverse
Restrict A∘M to the true range of M, then apply the inverse of M.equivRange. This constructs T before u and proves MT=AM. The actual conditional projection is contractive and reflection is an isometry, so ‖Tu‖=‖AMu‖=‖PU Mu‖≤‖u‖. No inverse or coherence certificate is supplied by a caller.
- 4Identify the literal source conditional integral and its AE fibers
Gaussian reflection preserves J, hence the true Λ has both marginals ν and S leaves ν invariant. The genuine posterior producer supplies an actual disintegration R0, whose every-y tilt agrees with the R1 in the real ReflectionL2 projection formula. Conditional-kernel uniqueness identifies it with the R from the same S producer AE ν. Actual UMu=u(2x−y) AE J transfers to conditional R fibers after the swap, and S_y=R_y.map(x↦2x−y) turns the P kernel formula into Tu=∫u dS_y AE ν. Stationarity and global u,u² integrability give only AE fiber integrability, as required for rough inputs.
- 5Use Fubini and the actual orthogonal block defect
AE square integrability supplies the real fiber variance identity Var(S_y,u)=∫u²dS_y−(Tu(y))². Stationarity and Fubini yield the first integrated second moment ∫u²dν; bounded T yields integrability of its square. Therefore the integrated variance is ‖u‖²−‖Tu‖². The genuine joint-L2 parent block identity applied to PMu=Mu identifies exactly the same quantity with ‖BMu‖². No expectation of an unbounded algorithmic cost is inferred.
- 6Exercise rough differences and a noncentered constant
The genuine Test applies the same bounded T to arbitrary u−v in L2, obtaining ‖Tu−Tv‖≤‖u−v‖, the exact variance defect, and its nonnegative bound by ‖u−v‖². The difference is explicitly an Lp class before selecting a representative, to avoid silently replacing it by a pointwise subtraction. The actual source-rank0 constant1 is fixed by T and has integrated variance0. The first coercion failure and actual correction are retained.
Full assumptions and notation
All objects and hypotheses
- Finite real Hilbert/Borel E and canonical volume; rank zero is an explicit extension of the source Euclidean presentation.
- V is C2; α,β≥0, α>0, α≤β, both global Hessian bounds; η>0 and βη≤1.
- Every u is an arbitrary real square-integrable AE class under the actual ν. No centering, compact support, extra moment, pointwise smoothness or caller normalization/operator/domain certificate.
- One genuine S,U,M,T is produced uniformly before u. Every-y normalized source law differs from AE ν fiber integrability and mean equality.
Mathematical proof
1. Use the same laws and the actual second-coordinate pullback
The existing macroscopic-energy theorem supplies μ,J,ν probability and genuine S,U,P on the exact source laws, including literal every-y S identity and compact-observer coherence. Since ν=J.snd, snd is measure preserving from J to ν. Mathlib constructs its canonical linear isometry M and the AE pullback representative. This is an actual map between full L2 spaces, not a finite-dimensional Lp assumption.
Corresponding Lean step
MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks; Lp.compMeasurePreservingₗᵢ; hM
2. Pass the true compact coherence to all L2 inputs
The existing actual Gaussian-marginal gradient core has dense smoothcompact domain. For its compact representative f, the real macroscopic parent supplies g=f∘snd, Pg=g and Ag=(Tf)∘snd, with Tf genuinely L2. Canonical AE uniqueness gives Mu=g and AMu=M[Tf]. The isometry has closed range because L2 is complete. PM=M is a closed equality and AMu∈rangeM a closed preimage; density extends both properties to every u.
Corresponding Lean step
GaussianMarginalGradient.gaussian_marginal_gradient_closable; hCore; Dense.induction; M.isometry.isClosedEmbedding; hPM; hAM
3. Construct one bounded operator by the closed-range inverse
Restrict A∘M to the true range of M, then apply the inverse of M.equivRange. This constructs T before u and proves MT=AM. The actual conditional projection is contractive and reflection is an isometry, so ‖Tu‖=‖AMu‖=‖PU Mu‖≤‖u‖. No inverse or coherence certificate is supplied by a caller.
Corresponding Lean step
ContinuousLinearMap.codRestrict; M.equivRange.symm; T; hMT; norm_condExpL2_coe_le; hTn
4. Identify the literal source conditional integral and its AE fibers
Gaussian reflection preserves J, hence the true Λ has both marginals ν and S leaves ν invariant. The genuine posterior producer supplies an actual disintegration R0, whose every-y tilt agrees with the R1 in the real ReflectionL2 projection formula. Conditional-kernel uniqueness identifies it with the R from the same S producer AE ν. Actual UMu=u(2x−y) AE J transfers to conditional R fibers after the swap, and S_y=R_y.map(x↦2x−y) turns the P kernel formula into Tu=∫u dS_y AE ν. Stationarity and global u,u² integrability give only AE fiber integrability, as required for rough inputs.
Corresponding Lean step
GaussianReflection.reflection_preserves_augmentation; GaussianConditionalKernel.exists_tilted_isCondKernel; ReflectionL2.actual_reflection_block_identities; hR₀R; hSource; hfs
5. Use Fubini and the actual orthogonal block defect
AE square integrability supplies the real fiber variance identity Var(S_y,u)=∫u²dS_y−(Tu(y))². Stationarity and Fubini yield the first integrated second moment ∫u²dν; bounded T yields integrability of its square. Therefore the integrated variance is ‖u‖²−‖Tu‖². The genuine joint-L2 parent block identity applied to PMu=Mu identifies exactly the same quantity with ‖BMu‖². No expectation of an unbounded algorithmic cost is inferred.
Corresponding Lean step
variance_eq_integral; variance_eq_sub; Measure.integral_compProd; hvarEq; hsecond; L2.inner_def; hDef; hvarDef
6. Exercise rough differences and a noncentered constant
The genuine Test applies the same bounded T to arbitrary u−v in L2, obtaining ‖Tu−Tv‖≤‖u−v‖, the exact variance defect, and its nonnegative bound by ‖u−v‖². The difference is explicitly an Lp class before selecting a representative, to avoid silently replacing it by a pointwise subtraction. The actual source-rank0 constant1 is fixed by T and has integrated variance0. The first coercion failure and actual correction are retained.
Corresponding Lean step
Tests.ProximalBPSL2MacroscopicMean.actual_rough_difference_variance; rank_zero_actual_source_constant
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_macroscopic_l2_mean
Use the same laws and the actual second-coordinate pullback; Pass the true compact coherence to all L2 inputs; Construct one bounded operator by the closed-range inverse; Identify the literal source conditional integral and its AE fibers; Use Fubini and the actual orthogonal block defect; Exercise rough differences and a noncentered constant
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_l2_mean
{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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
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 μ ∧ IsProbabilityMeasure J ∧ IsProbabilityMeasure ν ∧
∃ S : Kernel E E, IsMarkovKernel S ∧
(∀ y, S y = (volume : Measure E).tilted
(fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))) ∧
Λ.IsCondKernel S ∧ Λ.fst = ν ∧ Λ.snd = ν ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
∃ M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ u : Lp ℝ 2 ν, (M u : E × E → ℝ) =ᵐ[J] u ∘ Prod.snd) ∧
∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
let A := P * U.toContinuousLinearMap * P
let B := (1-P) * U.toContinuousLinearMap * P
∀ u : Lp ℝ 2 ν,
P (M u) = M u ∧ M (T u) = A (M u) ∧ ‖T u‖ ≤ ‖u‖ ∧
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) ∧
(∀ᵐ y ∂ν, Integrable (u : E → ℝ) (S y) ∧
Integrable (fun x => (u x)^2) (S y)) ∧
Integrable (fun y =>
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
(S y) (u : E → ℝ)) ν ∧
(∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
(S y) (u : E → ℝ) ∂ν) = ‖B (M u)‖^2 ∧
‖B (M u)‖^2 = ‖u‖^2-‖T u‖^2 := by
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 Λ := J.map (fun p : E × E => (p.2,(2 : ℝ) • p.1-p.2))
let F := fun p : E × E => (p.1,(2 : ℝ) • p.1-p.2)
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
obtain ⟨hμ,hJ,hν,R,S,hR,hS,hRc,hSr,hSd,hSc,hSf,U,hU,hUi,hUs,hops⟩ :=
MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks hα hαβ hV hH hη hβη
let : IsProbabilityMeasure μ := hμ
let : IsProbabilityMeasure J := hJ
let : IsProbabilityMeasure ν := hν
obtain ⟨hBA,hBD,hdef,hcompact⟩ := hops
let A := P * U.toContinuousLinearMap * P
have hp : MeasurePreserving (Prod.snd : E × E → E) J ν := ⟨measurable_snd,rfl⟩
let M : Lp ℝ 2 ν →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hp
have hM (u : Lp ℝ 2 ν) : (M u : E × E → ℝ) =ᵐ[J] u ∘ Prod.snd :=
Lp.coeFn_compMeasurePreserving u hp
obtain ⟨D,hDense,hClose,hClosed,hGraph⟩ :=
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient.gaussian_marginal_gradient_closable μ hη
have hCore (u : Lp ℝ 2 ν) (hu : u ∈ D.domain) :
P (M u) = M u ∧ A (M u) ∈ M.toLinearMap.range := by
obtain ⟨f,hf,hfc,huf,hdf⟩ := (hGraph u (D ⟨u,hu⟩)).mp (D.mem_graph ⟨u,hu⟩)
obtain ⟨hTd,hfLp,hTfLp,hgrad,hvar,g,hg,hPg,hAg,hn,hAn,hvb,hEnergy⟩ := hcompact f hf hfc
have hufJ : (fun p : E × E => u p.2) =ᵐ[J] (fun p => f p.2) :=
ae_of_ae_map measurable_snd.aemeasurable huf
have hMg : M u = g := Lp.ext ((hM u).trans (hufJ.trans hg.symm))
refine ⟨by rw [hMg]; exact hPg, ?_⟩
let v := hTfLp.toLp (fun y => ∫ x, f x ∂S y)
have hvJ : (fun p : E × E => v p.2) =ᵐ[J]
(fun p => ∫ x, f x ∂S p.2) :=
ae_of_ae_map measurable_snd.aemeasurable hTfLp.coeFn_toLp
have hAv : A (M u) = M v := by
rw [hMg]
exact Lp.ext (hAg.trans ((hM v).trans hvJ).symm)
exact ⟨v,hAv.symm⟩
have hPM (u : Lp ℝ 2 ν) : P (M u) = M u := by
exact hDense.induction (P := fun v => P (M v) = M v)
(fun v hv => (hCore v hv).1)
(isClosed_eq (P.continuous.comp M.continuous) M.continuous) u
have hAM (u : Lp ℝ 2 ν) : A (M u) ∈ M.toLinearMap.range := by
exact hDense.induction (P := fun v => A (M v) ∈ M.toLinearMap.range)
(fun v hv => (hCore v hv).2)
(M.isometry.isClosedEmbedding.isClosed_range.preimage (A.continuous.comp M.continuous)) u
let Ar := (A.comp M.toContinuousLinearMap).codRestrict M.toLinearMap.range hAM
let T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν :=
M.equivRange.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp Ar
have hMT (u : Lp ℝ 2 ν) : M (T u) = A (M u) := by
have he := M.equivRange.apply_symm_apply (Ar u)
exact congrArg Subtype.val he
have hPn (v : Lp ℝ 2 J) : ‖P v‖ ≤ ‖v‖ :=
norm_condExpL2_coe_le measurable_snd.comap_le v
have hTn (u : Lp ℝ 2 ν) : ‖T u‖ ≤ ‖u‖ := by
calc
‖T u‖ = ‖M (T u)‖ := (M.norm_map _).symm
_ = ‖A (M u)‖ := by rw [hMT]
_ = ‖P (U (M u))‖ := by
change ‖P (U (P (M u)))‖ = ‖P (U (M u))‖
rw [hPM]
_ ≤ ‖U (M u)‖ := hPn _
_ = ‖u‖ := by rw [U.norm_map,M.norm_map]
let : IsMarkovKernel R := hR
let : IsMarkovKernel S := hS
let : (J.map Prod.swap).IsCondKernel R := hRc
let : Λ.IsCondKernel S := hSc
obtain ⟨hFi,hFmap⟩ := GaussianReflection.reflection_preserves_augmentation μ η hη
have hFm : Measurable F := by fun_prop
have hFp : MeasurePreserving F J J := ⟨hFm,hFmap⟩
have hΛsnd : Λ.snd = ν := by
calc
Λ.snd = (J.map F).snd := by
dsimp only [Λ,Measure.snd]
rw [Measure.map_map measurable_snd (by fun_prop),Measure.map_map measurable_snd hFm]
rfl
_ = ν := by rw [hFmap]
have hcompS : ν ⊗ₘ S = Λ := by
calc
ν ⊗ₘ S = Λ.fst ⊗ₘ S := congrArg (fun ρ => ρ ⊗ₘ S) hSf.symm
_ = Λ := Measure.disintegrate Λ S
have hstation : S ∘ₘ ν = ν := by
rw [← Measure.snd_compProd,hcompS]
exact hΛsnd
obtain ⟨R₀,hR₀,hR₀d,hR₀c⟩ :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
let : IsMarkovKernel R₀ := hR₀
let : (J.map Prod.swap).IsCondKernel R₀ := hR₀c
obtain ⟨R₁,hR₁,hR₁d,U₁,hU₁,hUi₁,hUs₁,hPk,hAlgebra₁⟩ :=
ReflectionL2.actual_reflection_block_identities μ hη
have hR₁₀ : R₁ = R₀ := by
ext y s hs
rw [hR₁d y,hR₀d y]
have hR₀R : R₀ =ᵐ[ν] R := by
have h₀ : R₀ =ᵐ[(J.map Prod.swap).fst] (J.map Prod.swap).condKernel := eq_condKernel_of_measure_eq_compProd R₀ (Measure.disintegrate (J.map Prod.swap) R₀).symm
have hr : R =ᵐ[(J.map Prod.swap).fst] (J.map Prod.swap).condKernel := eq_condKernel_of_measure_eq_compProd R (Measure.disintegrate (J.map Prod.swap) R).symm
simpa only [Measure.fst_map_swap] using (Filter.EventuallyEq.trans h₀ (Filter.EventuallyEq.symm hr))
have hR₁R : R₁ =ᵐ[ν] R := by rw [hR₁₀]; exact hR₀R
have hSource (u : Lp ℝ 2 ν) :
(T u : E → ℝ) =ᵐ[ν] (fun y => ∫ x, u x ∂S y) := by
have huS : Integrable (u : E → ℝ) (S ∘ₘ ν) := by
rw [hstation]
exact (Lp.memLp u).integrable (by norm_num)
have hfiberS := Measure.ae_integrable_of_integrable_comp huS
have hUM : (U (M u) : E × E → ℝ) =ᵐ[J]
(fun p => u ((2 : ℝ) • p.1-p.2)) :=
(hU (M u)).trans (hFp.quasiMeasurePreserving.ae_eq (hM u))
have hswap : (fun p : E × E => (U (M u)) (p.2,p.1)) =ᵐ[J.map Prod.swap]
(fun p => u ((2 : ℝ) • p.2-p.1)) := by
change ∀ᵐ p ∂J.map (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E),
(U (M u)) (p.2,p.1) = u ((2 : ℝ) • p.2-p.1)
rw [← (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E).map_ae]
change ∀ᵐ p ∂J, (U (M u)) p = u ((2 : ℝ) • p.1-p.2)
exact hUM
have hswap' : (fun p : E × E => (U (M u)) (p.2,p.1)) =ᵐ[ν ⊗ₘ R]
(fun p => u ((2 : ℝ) • p.2-p.1)) := by
have hcR : ν ⊗ₘ R = J.map Prod.swap := by
simpa only [Measure.fst_map_swap] using Measure.disintegrate (J.map Prod.swap) R
rw [hcR]
exact hswap
have hfiberR := Measure.ae_ae_of_ae_compProd hswap'
have hSourceJ : (fun p : E × E => (T u) p.2) =ᵐ[J]
(fun p => ∫ x, u x ∂S p.2) := by
have hMTae : (M (T u) : E × E → ℝ) =ᵐ[J]
(fun p => ∫ x, (U (M u)) (x,p.2) ∂R₁ p.2) := by
rw [hMT]
change (P (U (P (M u))) : E × E → ℝ) =ᵐ[J] _
rw [hPM]
exact hPk (U (M u))
have hkJ := ae_of_ae_map measurable_snd.aemeasurable hR₁R
have hfJ := ae_of_ae_map measurable_snd.aemeasurable hfiberR
have hfiJ := ae_of_ae_map measurable_snd.aemeasurable hfiberS
filter_upwards [(hM (T u)).symm.trans hMTae,hkJ,hfJ,hfiJ] with p hmean hk hf hfi
change (T u) p.2 = ∫ x, (U (M u)) (x,p.2) ∂R₁ p.2 at hmean
rw [hmean,hk,integral_congr_ae hf,hSr p.2]
exact (integral_map (by fun_prop) (by simpa only [hSr p.2] using hfi.aestronglyMeasurable)).symm
exact (ae_map_iff measurable_snd.aemeasurable
(measurableSet_eq_fun (Lp.stronglyMeasurable (T u)).measurable
((Lp.stronglyMeasurable u).integral_kernel.measurable))).mpr hSourceJ
let B := (1-P) * U.toContinuousLinearMap * P
refine ⟨hμ,hJ,hν,S,hS,hSd,hSc,hSf,hΛsnd,U,hU,hUi,hUs,M,hM,T,?_⟩
intro u
have huS : Integrable (u : E → ℝ) (S ∘ₘ ν) := by
rw [hstation]
exact (Lp.memLp u).integrable (by norm_num)
have huSqS : Integrable (fun x => (u x)^2) (S ∘ₘ ν) := by
rw [hstation]
exact (Lp.memLp u).integrable_sq
have hfS := Measure.ae_integrable_of_integrable_comp huS
have hfSqS := Measure.ae_integrable_of_integrable_comp huSqS
have hfs : ∀ᵐ y ∂ν, Integrable (u : E → ℝ) (S y) ∧
Integrable (fun x => (u x)^2) (S y) := hfS.and hfSqS
have hmean := hSource u
let m := fun y => ∫ x, u x ∂S y
have hmLp : MemLp m 2 ν := MemLp.ae_eq hmean (Lp.memLp (T u))
have hsqI : Integrable (fun y => ∫ x, (u x)^2 ∂S y) ν := by
have hi := Measure.integrable_integral_norm_of_integrable_comp huSqS
simpa only [Real.norm_eq_abs,abs_pow,sq_abs] using hi
have hvarEq : (fun y => AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
(S y) (u : E → ℝ)) =ᵐ[ν] (fun y => (∫ x, (u x)^2 ∂S y)-(m y)^2) := by
filter_upwards [hfSqS] with y hy
have hLpY := (memLp_two_iff_integrable_sq (Lp.stronglyMeasurable u).aestronglyMeasurable).mpr hy
dsimp only [AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance,m]
rw [← variance_eq_integral hLpY.aemeasurable,variance_eq_sub hLpY]
rfl
have hvarI : Integrable (fun y =>
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance (S y) (u : E → ℝ)) ν :=
(hsqI.sub hmLp.integrable_sq).congr hvarEq.symm
have hsecond : (∫ y, ∫ x, (u x)^2 ∂S y ∂ν) = ∫ x, (u x)^2 ∂ν := by
have hj : Integrable (fun p : E × E => (u p.2)^2) (ν ⊗ₘ S) := by
rw [hcompS]
apply ((Lp.memLp u).comp_measurePreserving
(show MeasurePreserving (Prod.snd : E × E → E) Λ ν from ⟨measurable_snd,hΛsnd⟩)).integrable_sq
rw [← Measure.integral_compProd hj,hcompS]
calc
(∫ p : E × E, (u p.2)^2 ∂Λ) = ∫ x, (u x)^2 ∂Λ.snd :=
(integral_map (μ := Λ) measurable_snd.aemeasurable
(f := fun x => (u x)^2) ((Lp.stronglyMeasurable u).pow 2).aestronglyMeasurable).symm
_ = ∫ x, (u x)^2 ∂ν := by rw [hΛsnd]
have hn (v : Lp ℝ 2 ν) : ‖v‖^2 = ∫ y, (v y)^2 ∂ν := by
calc
‖v‖^2 = inner ℝ v v := (real_inner_self_eq_norm_sq v).symm
_ = ∫ y, (v y)^2 ∂ν := by rw [L2.inner_def]; simp only [real_inner_self_eq_norm_sq,Real.norm_eq_abs,sq_abs]
have hDef : ‖B (M u)‖^2 = ‖u‖^2-‖T u‖^2 := by
calc
‖B (M u)‖^2 = ‖M u‖^2-‖A (M u)‖^2 := hdef _ (hPM u)
_ = ‖u‖^2-‖T u‖^2 := by rw [M.norm_map,← hMT,M.norm_map]
have hvarDef : (∫ y,
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance (S y) (u : E → ℝ) ∂ν) =
‖B (M u)‖^2 := by
rw [integral_congr_ae hvarEq,integral_sub hsqI hmLp.integrable_sq,hsecond,hDef,hn u,hn (T u)]
congr 1
exact (integral_congr_ae (Filter.EventuallyEq.fun_comp hmean (fun x : ℝ => x^2))).symm
exact ⟨hPM u,hMT u,hTn u,hmean,hfs,hvarI,hvarDef,hDef⟩
end AutoSamplingTheory.ExampleCases.ProximalBPS.L2MacroscopicMeanScope and omitted-condition boundaries
- One actual canonical snd pullback M and bounded conditional mean T are chosen before every rough L2 input under the SAME Gibbs/Gaussian laws. PM=M, MT=AM, true AE source-S mean, contraction, AE fiber L1/squareL1 and integrated variance=||BMu||²=||u||²-||Tu||² are proved internally. Original C2/two-sided Hessian/capped step retained; finite Hilbert/Borel/rank0 explicitly extends the source Euclidean setting. No every-y rough integrability/C1, gradient/H1/B13, Gamma/dynamics/main/errors/unbounded-cost or actual-input composition claim.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy.actual_macroscopic_gradient_energy_blocksAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient.gaussian_marginal_gradient_closableAutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2.actual_reflection_block_identitiesAutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentationAutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel
Mathlib API called (external library)
- Lp.compMeasurePreservingₗᵢ
- Lp.coeFn_compMeasurePreserving
- Dense.induction
- LinearIsometry.equivRange
- ContinuousLinearMap.codRestrict
- norm_condExpL2_coe_le
- Measure.integral_compProd
- variance_eq_sub
Mathematical sources
- PBPS2609.06905v1 Appendix B.1 real conditional projection/reflection blocks and B.9 variance identity; actual all-L2 mean bridge needed before full rough B.13. Source C2 potential, both Hessian bounds and capped positive step retained. — One actual canonical snd pullback M and bounded conditional mean T are chosen before every rough L2 input under the SAME Gibbs/Gaussian laws. PM=M, MT=AM, true AE source-S mean, contraction, AE fiber L1/squareL1 and integrated variance=||BMu||²=||u||²-||Tu||² are proved internally. Original C2/two-sided Hessian/capped step retained; finite Hilbert/Borel/rank0 explicitly extends the source Euclidean setting. No every-y rough integrability/C1, gradient/H1/B13, Gamma/dynamics/main/errors/unbounded-cost or actual-input composition 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.