Actual reflection and conditional-projection blocks
AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2.actual_reflection_block_identities · theorem · Teaching coverage
Mathematical statement
There is a Markov kernel R with R_y=μ tilted by −‖x−y‖²/(2η), and a real linear isometry U with Uf=f∘F almost everywhere, U²=I and U*=U. For every L² class f, Pf(x,y)=∫f(x′,y)R_y(dx′) J-almost everywhere. The actual blocks obey B*B=P−A² and B*D=−AB*. For every Pf=f, ‖Bf‖²=‖f‖²−‖Af‖².
Lean statement · actual_reflection_block_identities
All ambient spaces, μ and η are quantified. The joint law, reflection and conditional projection are local definitions. R and U are constructed witnesses with actual-law semantics.
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_reflection_block_identities
{E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η) :
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
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
∃ R : Kernel E E, IsMarkovKernel R ∧
(∀ y, R y = μ.tilted (fun x => -‖x-y‖^2/(2*η))) ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ f, U f =ᵐ[J] f ∘ F) ∧ Function.Involutive U ∧
IsSelfAdjoint U.toContinuousLinearMap ∧
(∀ f : Lp ℝ 2 J, (P f : E × E → ℝ) =ᵐ[J]
fun p => ∫ x, f (x,p.2) ∂R p.2) ∧
let A := P * U.toContinuousLinearMap * P
let B := (1-P) * U.toContinuousLinearMap * P
let D := (1-P) * U.toContinuousLinearMap * (1-P)
star B*B=P-A^2 ∧ star B*D= -(A*star B) ∧
(∀ f, P f=f → ‖B f‖^2 = ‖f‖^2-‖A f‖^2)Proof roadmap
- 1Lift the actual reflection
The Gaussian augmentation is preserved by F, and F∘F=id. Pullback therefore preserves L² norms and defines a linear isometry U on equivalence classes. Applying the involution twice gives U²=I. Inner-product preservation implies ⟨Uf,g⟩=⟨f,Ug⟩, hence U*=U.
- 2Identify the conditional projection
The proved quadratic-tilt kernel disintegrates the swapped joint law (Y,X). Conditional-distribution integration and a.e. uniqueness of disintegration identify the conditional expectation given Y. Since J is a probability measure, each L² representative is integrable. The L² conditional expectation agrees a.e. with this integral, so the actual orthogonal projection has the stated kernel semantics.
- 3Expand the diagonal and off-diagonal blocks
Write Q=I−P. Orthogonal projection gives P*=P and P²=P. Thus B*B=PUQUP=PU²P−PUPUP=P−A². Also B*D=PUQUQ=PU²Q−PUPUQ=−AB*, using PQ=0. These are identities on the whole Hilbert space; P becomes the identity only on its range.
- 4Recover the energy transferred from the macroscopic space
The compression A is self-adjoint. For Pf=f, take the inner product of B*B=P−A² with f. The P term is ‖f‖² and self-adjointness changes ⟨f,A²f⟩ into ‖Af‖². No centering or spectral-gap premise is needed for this algebraic identity.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional real inner-product space with its Borel measurable structure; dimension zero is allowed. μ is any probability measure on E and η>0.
- J is the law of (X,X+sqrt(η)Z), with independent X of law μ and standard Gaussian Z. All operators act on the real Hilbert space L²(J).
- F(x,y)=(x,2x−y). P is the inclusion into L²(J) of conditional expectation onto the sub-sigma-algebra generated by Y; P is defined, not assumed.
- Let A=PUP, B=(I−P)UP and D=(I−P)U(I−P), with multiplication denoting composition. The energy identity quantifies over every f satisfying Pf=f.
Mathematical proof
1. Lift the actual reflection
The Gaussian augmentation is preserved by F, and F∘F=id. Pullback therefore preserves L² norms and defines a linear isometry U on equivalence classes. Applying the involution twice gives U²=I. Inner-product preservation implies ⟨Uf,g⟩=⟨f,Ug⟩, hence U*=U.
Corresponding Lean step
reflection_lift uses the proved measure-preserving reflection and Lp.compMeasurePreservingₗᵢ.
2. Identify the conditional projection
The proved quadratic-tilt kernel disintegrates the swapped joint law (Y,X). Conditional-distribution integration and a.e. uniqueness of disintegration identify the conditional expectation given Y. Since J is a probability measure, each L² representative is integrable. The L² conditional expectation agrees a.e. with this integral, so the actual orthogonal projection has the stated kernel semantics.
Corresponding Lean step
kernel_condExp and projection_kernel use condExp_prod_ae_eq_integral_condDistrib', eq_condKernel_of_measure_eq_compProd and MemLp.condExpL2_ae_eq_condExp. No everywhere assertion for arbitrary representatives is made.
3. Expand the diagonal and off-diagonal blocks
Write Q=I−P. Orthogonal projection gives P*=P and P²=P. Thus B*B=PUQUP=PU²P−PUPUP=P−A². Also B*D=PUQUQ=PU²Q−PUPUQ=−AB*, using PQ=0. These are identities on the whole Hilbert space; P becomes the identity only on its range.
Corresponding Lean step
block_algebra proves both identities from the established projection and reflection equalities by noncommutative ring normalization.
4. Recover the energy transferred from the macroscopic space
The compression A is self-adjoint. For Pf=f, take the inner product of B*B=P−A² with f. The P term is ‖f‖² and self-adjointness changes ⟨f,A²f⟩ into ‖Af‖². No centering or spectral-gap premise is needed for this algebraic identity.
Corresponding Lean step
block_energy uses the adjoint norm identity and the actual compression self-adjointness.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_reflection_block_identities
Five local proof helpers feed one public theorem. The test rewrites the actual Gibbs normalized density to its generative augmentation using normalized_augmentation_density; positive normalization supplies integrability and the probability instance.
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_reflection_block_identities
{E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η) :
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
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
∃ R : Kernel E E, IsMarkovKernel R ∧
(∀ y, R y = μ.tilted (fun x => -‖x-y‖^2/(2*η))) ∧
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ f, U f =ᵐ[J] f ∘ F) ∧ Function.Involutive U ∧
IsSelfAdjoint U.toContinuousLinearMap ∧
(∀ f : Lp ℝ 2 J, (P f : E × E → ℝ) =ᵐ[J]
fun p => ∫ x, f (x,p.2) ∂R p.2) ∧
let A := P * U.toContinuousLinearMap * P
let B := (1-P) * U.toContinuousLinearMap * P
let D := (1-P) * U.toContinuousLinearMap * (1-P)
star B*B=P-A^2 ∧ star B*D= -(A*star B) ∧
(∀ f, P f=f → ‖B f‖^2 = ‖f‖^2-‖A f‖^2) := by
let J₀ := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
let H := Lp ℝ 2 J₀
have reflection_lift (μ : Measure E) [IsProbabilityMeasure μ] (η : ℝ) (hη : 0 < η) :
let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
let R := fun p : E × E => (p.1, (2:ℝ) • p.1-p.2)
∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
(∀ f, U f =ᵐ[J] f ∘ R) ∧ Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap := by
dsimp only
let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
let R := fun p : E × E => (p.1, (2:ℝ) • p.1-p.2)
obtain ⟨hinv, hmap⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentation μ η hη
have hp : MeasurePreserving R J J := ⟨by fun_prop, hmap⟩
let U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J := Lp.compMeasurePreservingₗᵢ ℝ R hp
have hU : Function.Involutive U := by
intro f
change Lp.compMeasurePreserving R hp (Lp.compMeasurePreserving R hp f) = f
rw [← Lp.compMeasurePreserving_comp_apply]
have hRR : R ∘ R = id := funext hinv
simp only [hRR, Lp.compMeasurePreserving_id_apply]
refine ⟨U, fun f => Lp.coeFn_compMeasurePreserving f hp, hU, ?_⟩
apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.2
intro f g
change inner ℝ (U f) g = inner ℝ f (U g)
calc
inner ℝ (U f) g = inner ℝ (U f) (U (U g)) := by rw [hU g]
_ = inner ℝ f (U g) := U.inner_map_map f (U g)
have kernel_condExp (J : Measure (E × E)) [IsProbabilityMeasure J]
(R : Kernel E E) [IsMarkovKernel R] [(J.map Prod.swap).IsCondKernel R]
(f : E × E → ℝ) (hf : Integrable f J) :
J[f | MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)] =ᵐ[J]
fun p => ∫ x, f (x,p.2) ∂R p.2 := by
have hswap : Integrable (fun p : E × E => f p.swap) (J.map Prod.swap) := by
apply (integrable_map_equiv (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E) _).2
change Integrable f J
exact hf
have h := condExp_prod_ae_eq_integral_condDistrib'
(μ := J) (X := Prod.snd) (Y := Prod.fst)
(f := fun p : E × E => f p.swap) measurable_snd measurable_fst.aemeasurable hswap
have heq : R =ᵐ[(J.map Prod.swap).fst] (J.map Prod.swap).condKernel :=
eq_condKernel_of_measure_eq_compProd R (Measure.disintegrate _ _).symm
rw [Measure.fst_map_swap] at heq
have heq' : ∀ᵐ p ∂J, R p.2 = (J.map Prod.swap).condKernel p.2 := by
exact ae_of_ae_map measurable_snd.aemeasurable heq
filter_upwards [h, heq'] with p hp he
rw [he]
simp only [condDistrib] at hp
exact hp
have projection_kernel (μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η) :
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
∃ R : Kernel E E, IsMarkovKernel R ∧
(∀ y, R y = μ.tilted (fun x => -‖x-y‖^2/(2*η))) ∧
(∀ f : Lp ℝ 2 J,
(condExpL2 ℝ ℝ (μ := J) measurable_snd.comap_le f : E × E → ℝ) =ᵐ[J]
fun p => ∫ x, f (x,p.2) ∂R p.2) := by
dsimp only
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
have : IsProbabilityMeasure J := Measure.isProbabilityMeasure_map (by fun_prop)
obtain ⟨R,hR,hformula,hcond⟩ :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
let _ := hR
let _ : (J.map Prod.swap).IsCondKernel R := hcond
refine ⟨R,hR,hformula,?_⟩
intro f
have hL2 := (Lp.memLp f).condExpL2_ae_eq_condExp (𝕜 := ℝ) measurable_snd.comap_le
rw [Lp.toLp_coeFn] at hL2
exact hL2.trans (kernel_condExp J R f ((Lp.memLp f).integrable (by norm_num)))
have block_algebra {A : Type u} [Ring A] [StarRing A] (U P : A)
(hU : star U = U) (hP : star P = P) (hUU : U*U=1) (hPP : P*P=P) :
let B := (1-P)*U*P
let D := (1-P)*U*(1-P)
let A₀ := P*U*P
star B*B=P-A₀^2 ∧ star B*D= -(A₀*star B) := by
have hpt (X : A) : P*(P*X)=P*X := by rw [← mul_assoc,hPP]
have hut (X : A) : U*(U*X)=X := by rw [← mul_assoc,hUU,one_mul]
dsimp only
simp only [star_mul,star_sub,star_one,hU,hP]
constructor <;> noncomm_ring [hPP,hUU,hpt,hut]
have block_energy (P A B : H →L[ℝ] H) (hA : IsSelfAdjoint A)
(hBB : star B * B = P-A^2) (f : H) (hf : P f=f) :
‖B f‖^2 = ‖f‖^2-‖A f‖^2 := by
have h := B.apply_norm_sq_eq_inner_adjoint_right f
have he : B.adjoint.comp B = P-A^2 := hBB
rw [he] at h
have hAf : inner ℝ f ((A^2) f) = ‖A f‖^2 := by
rw [pow_two]
change inner ℝ f (A (A f)) = _
calc
inner ℝ f (A (A f)) = inner ℝ f (A.adjoint (A f)) := by rw [hA.adjoint_eq]
_ = inner ℝ (A f) (A f) := A.adjoint_inner_right f (A f)
_ = ‖A f‖^2 := real_inner_self_eq_norm_sq (A f)
simpa only [sub_apply, hf, inner_sub_right,
hAf, real_inner_self_eq_norm_sq, RCLike.re_to_real] using h
dsimp only
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
(μ.prod (stdGaussian E))
let mY : MeasurableSpace (E × E) := MeasurableSpace.comap Prod.snd (inferInstance : MeasurableSpace E)
let _ : MeasurableSpace (E × E) := Prod.instMeasurableSpace
have hmY : mY ≤ Prod.instMeasurableSpace := measurable_snd.comap_le
let S := lpMeas ℝ ℝ mY 2 J
have : Fact (mY ≤ Prod.instMeasurableSpace) := ⟨hmY⟩
let P : Lp ℝ 2 J →L[ℝ] Lp ℝ 2 J := S.subtypeL ∘L condExpL2 ℝ ℝ (μ := J) hmY
have hPdef : P = S.starProjection := rfl
have hP : IsSelfAdjoint P := by rw [hPdef]; exact isSelfAdjoint_starProjection S
have hPP : P*P=P := by rw [hPdef]; exact S.isIdempotentElem_starProjection
obtain ⟨U,hUae,hUi,hUs⟩ := reflection_lift μ η hη
obtain ⟨R,hR,hRf,hRp⟩ := projection_kernel μ hη
have hUU : U.toContinuousLinearMap * U.toContinuousLinearMap = 1 := by
apply ContinuousLinearMap.ext
intro f
exact hUi f
obtain ⟨hBB,hBD⟩ := block_algebra U.toContinuousLinearMap P hUs.star_eq hP.star_eq hUU hPP
have hA : IsSelfAdjoint (P*U.toContinuousLinearMap*P) := by
change star (P*U.toContinuousLinearMap*P) = P*U.toContinuousLinearMap*P
simp only [star_mul,hP.star_eq,hUs.star_eq,mul_assoc]
refine ⟨R,hR,hRf,U,hUae,hUi,hUs,hRp,hBB,hBD,?_⟩
intro f hf
exact block_energy P (P*U.toContinuousLinearMap*P) ((1-P)*U.toContinuousLinearMap*P) hA hBB f hf
end AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The paper uses the normalized Gibbs target on R^d, d≥1, with C² potential V and Hessian bounds 0<αI≤∇²V≤βI, and 0<η≤1/β. Its joint law has density proportional to exp(−V(x)−‖y−x‖²/(2η)). | E is a finite-dimensional real inner-product space with its Borel measurable structure; dimension zero is allowed. μ is any probability measure on E and η>0. | generalization | These algebraic identities need only an input probability and positive Gaussian scale, not curvature or an upper scale bound. The separately compiled Gibbs-density consumer retains C² and positive Hessian lower bound, derives normalization and specializes every conclusion on the explicit source density. Zero dimension is also valid. |
| Conditional projection is written with conditional-kernel representatives. | Integral representation is J-a.e. for every L² class. | source-implicit | Conditional expectation and L² classes are defined modulo null sets; arbitrary representatives need not have an everywhere-defined integrable section. Finite probability provides L²-to-L¹ integrability. |
| B*B=I−A² on the macroscopic subspace. | B*B=P−A² on the full Hilbert space, with Pf=f explicitly required in the energy clause. | same | Compressed blocks are extended by zero on the orthogonal complement; this retains the subspace identity without falsely replacing P by I everywhere. |
Actual reflection and conditional-projection block identities only. No macro coercivity, Sobolev regularity, square roots or inverses, half-turn process, invariance or nonexplosion, modified-energy contraction, mixing, implementation error, expected cost or full-paper closure.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Disclosed generalization to arbitrary probability input, including zero dimension. — Lesson and candidate assumptions disclose it; Gibbs consumer applies full result on exact source density.
- assumptions: Curvature and upper scale restrictions unnecessary for this algebra; no extension of full mixing claim. — Actual preservation, conditional kernel and orthogonal projection support proof; consumer supplies Gibbs normalization.
- scopes: Macroscopic identity represented as B*B=P−A² on full space. — Actual projection; block_energy retains Pf=f.
- quantifiers: A.e. representative formulas for each f, everywhere fiber formula for R. — Theorem, authored proof and anonymous reconstruction distinguish ∀y from ∀f a.e.
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
- Actual reflection and conditional-projection block identities only. No macro coercivity, Sobolev regularity, square roots or inverses, half-turn process, invariance or nonexplosion, modified-energy contraction, mixing, implementation error, expected cost or full-paper closure.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection.reflection_preserves_augmentationAutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel
Mathlib API called (external library)
- Lp.compMeasurePreservingₗᵢ
- condExpL2
- condExp_prod_ae_eq_integral_condDistrib'
- eq_condKernel_of_measure_eq_compProd
- isSelfAdjoint_starProjection
- Submodule.isIdempotentElem_starProjection
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS v1 Appendix B.1 — Equations B.1 and B.3–B.5, expanded actual-law proof.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.