ASTIS mathematical exposition

Actual reflection and conditional-projection blocks

AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2.actual_reflection_block_identities · theorem · Teaching coverage

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‖².

\[B^*B=P-A^2,\qquad B^*D=-AB^*,\qquad Pf=f\Longrightarrow\|Bf\|^2=\|f\|^2-\|Af\|^2.\]

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.

\[U^2=I,\quad\langle Uf,g\rangle=\langle Uf,U^2g\rangle=\langle f,Ug\rangle.\]

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.

\[(Pf)(x,y)=\int f(x^{\prime},y)R_y(dx^{\prime})\quad J\text{-a.e.}\]

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.

\[B^*B=PU(I-P)UP=P-A^2,\qquad B^*D=PU(I-P)U(I-P)=-AB^*.\]

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.

\[\|Bf\|^2=\langle f,(P-A^2)f\rangle=\|f\|^2-\|Af\|^2.\]

Corresponding Lean step

block_energy uses the adjoint norm identity and the actual compression self-adjointness.

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)

Exact module and namespace context

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.

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.ReflectionL2

Exact module and namespace context

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.

Source and reuse

ASTIS parents called

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.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.