Actual macroscopic reflection blocks and sharp smooth gradient energy

Source Appendix B.1-B.9 and C.1 (C.2), with authored A/B/D aliases and actual same-law/kernel/L² bookkeeping. Independently typed Statement Seal and independently reviewed source-only topology precede proof. Full B.13 rough-domain, Γ and main-cost results remain separate.

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C² and 0<α≤β, with α‖a‖²≤D²V(x)[a,a]≤β‖a‖² for every x,a. Suppose η>0 and βη≤1. Define μ as the normalized volume tilt exp(-V), J as the actual law of (X,X+√η G) for independent X∼μ and standard Gaussian G, ν=J.snd, Λ as the law of (Y,2X-Y), and F(x,y)=(x,2x-y). The theorem produces probability of μ,J,ν and common Markov kernels R,S, with swapped J disintegrated by R, every-y reflected S, its exact normalized density, and Λ=ν⊗S. On the actual Hilbert space L²(J), P is conditional projection given Y; one common U is the genuine reflection pullback, a self-adjoint isometric involution. With authored aliases A=PUP, B=(I-P)UP and D=(I-P)U(I-P), B*B=P-A² and B*D=-AB*. For every Pg=g, ‖Bg‖²=‖g‖²-‖Ag‖². For each signed smooth compactly supported f, the literal Tf(y)=∫f(u)S_y(du) is differentiable, f,Tf,∇Tf lie in L²(ν), and Var_Sf lies in L¹(ν). A genuine class g=[f∘snd] satisfies Pg=g and Ag=[Tf∘snd]; its actual squared norm and the squared norm of Ag equal ∫f²dν and ∫(Tf)²dν. Moreover ∫Var_Sf dν=‖Bg‖² and η∫‖∇Tf‖²dν≤(1-αη)²/[4(1+αη)]‖Bg‖². No centering or law, operator, representative, domain or bound certificate is a public assumption.

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 macroscopic reflection blocks and sharp smooth gradient energy

AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy.actual_macroscopic_gradient_energy_blocks · theorem · Teaching coverage

Read this first

Mathematical statement

\[\int\operatorname{Var}_{S_y}(f)\,\nu(dy)=\|Bg\|_{L^2(J)}^2=\|g\|_{L^2(J)}^2-\|Ag\|_{L^2(J)}^2,\qquad\eta\int\|\nabla Tf\|^2\,d\nu\le\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}\|Bg\|_{L^2(J)}^2.\]

Lean statement · actual_macroscopic_gradient_energy_blocks

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_gradient_energy_blocks
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E,
      (α : ℝ) * ‖a‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x a) a ∧
      (fderiv ℝ (fderiv ℝ V) x a) a ≤ (β : ℝ) * ‖a‖^2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    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 ν ∧
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2 : ℝ) • x - y)) ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun u => -V ((1/2 : ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧
      ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
        (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
        Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
        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) ∧
        (∀ g : Lp ℝ 2 J, P g = g → ‖B g‖^2 = ‖g‖^2 - ‖A g‖^2) ∧
        ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
          let Tf := fun y => ∫ u, f u ∂S y
          Differentiable ℝ Tf ∧ MemLp f 2 ν ∧ MemLp Tf 2 ν ∧
          MemLp (gradient Tf) 2 ν ∧
          Integrable (fun y =>
            AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
              (S y) f) ν ∧
          ∃ g : Lp ℝ 2 J,
            (g : E × E → ℝ) =ᵐ[J] (fun p => f p.2) ∧ P g = g ∧
            (A g : E × E → ℝ) =ᵐ[J] (fun p => Tf p.2) ∧
            ‖g‖^2 = (∫ y, (f y)^2 ∂ν) ∧
            ‖A g‖^2 = (∫ y, (Tf y)^2 ∂ν) ∧
            (∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
              (S y) f ∂ν) = ‖B g‖^2 ∧
            η * (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤
              (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) * ‖B g‖^2

Exact module and namespace context

Proof roadmap

1Keep one genuine conditional kernel and literal smooth mean
Reuse the genuine outer-energy producer to obtain μ,J,ν as probabilities and one common R,S before choosing f. The same S gives every-y reflection and normalized density. Its literal integral Tf already has genuine differentiability and all finite domains; these outputs stay attached to this S throughout.
2Produce the actual reflected-pair disintegration
Map the actual swapped-joint disintegration through (y,x)↦(y,2x-y). Measurability and the exact setwise kernel-map formula show that the resulting measure is ν⊗S and is precisely Λ. Its first coordinate is the actual ν; this is a derived law identity, not a caller premise.
3Use AE uniqueness only for conditional means and classes
The macroscopic representative parent has a kernel S₀ disintegrating the same Λ. Genuine conditional-kernel uniqueness gives S=S₀ almost everywhere under ν. Lift this equality along snd to J. It identifies integral values and L² representatives; it does not transport pointwise derivatives. We retain the original differentiable Tf from the first step.
4Identify the actual reflection operators and retain block algebra
Both producer isometries act on the same L²(J) by composition with F. Their AE actions agree, hence Lp extensionality identifies the isometries. This joins the actual macroscopic representative with the genuine reflection block identities, using the actual comap-snd projection P.
5Identify both actual second moments
The real Hilbert inner product expresses each squared L² norm as the integral of its representative squared. Use the actual AE representatives and ν=J.snd to transport the two moments. Continuity of f and of the genuine Tf supplies the measurable integral-map domain. No hypothetical squared-norm identity is assumed.
6Close the genuine microscopic variance identity
The outer-energy producer gives the exact integrated conditional variance defect. Substitute the two genuine second moments and the actual reflection-block norm defect for Pg=g. The same S therefore supplies the microscopic block norm-square.
7Join the exact smooth gradient bound
Substitute the genuine variance/block identity into the already proved sharp smooth energy estimate. Every domain and the actual Bg are now internal outputs. This is the smooth compact block input used toward B.13; it does not construct Γ or extend the gradient operator to arbitrary rough L² classes.
8Exercise zero energy and a noncentered class
At V=‖x‖²/2 and α=β=η=1, the sharp coefficient is zero and the actual smooth gradient energy vanishes. In rank zero the constant f=1 is smooth with compact support: its genuine class has norm-square one, Ag=g, and microscopic block/conditional variance/gradient energy zero. This verifies that no hidden centering premise entered the class or norm bridge.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert space E with Borel structure; rank zero is an explicit authored extension of the source Euclidean setting.
Globally C² potential V; 0<α≤β and the genuine pointwise Hessian bounds α‖a‖²≤D²V(x)[a,a]≤β‖a‖².
Positive step η with βη≤1, exactly the source restriction.
Signed smooth compactly supported f. All probabilities, kernels, L² classes, differentiability, L²/L¹ domains and block/variance identities are produced internally.

Mathematical proof

1. Keep one genuine conditional kernel and literal smooth mean

Reuse the genuine outer-energy producer to obtain μ,J,ν as probabilities and one common R,S before choosing f. The same S gives every-y reflection and normalized density. Its literal integral Tf already has genuine differentiability and all finite domains; these outputs stay attached to this S throughout.

\[Tf(y)=\int f(u)S_y(du),\quad S_y=(x\mapsto2x-y)_\#R_y,\quad\nabla Tf\in L^2(\nu).\]

Corresponding Lean step

ConditionalGradientEnergy.reflected_conditional_gradient_energy; henergy; hcond; hSR; hSd

2. Produce the actual reflected-pair disintegration

Map the actual swapped-joint disintegration through (y,x)↦(y,2x-y). Measurability and the exact setwise kernel-map formula show that the resulting measure is ν⊗S and is precisely Λ. Its first coordinate is the actual ν; this is a derived law identity, not a caller premise.

\[\Lambda=(y,2x-y)_\#(\nu\otimes R)=\nu\otimes S,\qquad\Lambda_\mathrm{fst}=\nu.\]

Corresponding Lean step

hG; hmap; hΛmap; hfst; hΛcond; Measure.compProd_apply; Measure.map_apply; Measure.disintegrate

3. Use AE uniqueness only for conditional means and classes

The macroscopic representative parent has a kernel S₀ disintegrating the same Λ. Genuine conditional-kernel uniqueness gives S=S₀ almost everywhere under ν. Lift this equality along snd to J. It identifies integral values and L² representatives; it does not transport pointwise derivatives. We retain the original differentiable Tf from the first step.

\[S=S_0\quad\nu\text{-a.e.},\qquad Tf(Y)=T_0f(Y)\quad J\text{-a.e.}.\]

Corresponding Lean step

eq_condKernel_of_measure_eq_compProd; hκ; ae_of_ae_map; hκJ; hAgS

4. Identify the actual reflection operators and retain block algebra

Both producer isometries act on the same L²(J) by composition with F. Their AE actions agree, hence Lp extensionality identifies the isometries. This joins the actual macroscopic representative with the genuine reflection block identities, using the actual comap-snd projection P.

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

Corresponding Lean step

MacroscopicRepresentative.macroscopic_reflection_smooth_representative; ReflectionL2.actual_reflection_block_identities; LinearIsometry.ext; Lp.ext; hUU; hBB; hBD; hblock

5. Identify both actual second moments

The real Hilbert inner product expresses each squared L² norm as the integral of its representative squared. Use the actual AE representatives and ν=J.snd to transport the two moments. Continuity of f and of the genuine Tf supplies the measurable integral-map domain. No hypothetical squared-norm identity is assumed.

\[g=[f\circ\mathrm{snd}],\quad Ag=[Tf\circ\mathrm{snd}],\quad\|g\|^2=\int f^2d\nu,\quad\|Ag\|^2=\int(Tf)^2d\nu.\]

Corresponding Lean step

norm_snd (fixed actual J/ν local adapter, twice consumed); L2.inner_def; real_inner_self_eq_norm_sq; integral_congr_ae; integral_map; hgn; hAgn

6. Close the genuine microscopic variance identity

The outer-energy producer gives the exact integrated conditional variance defect. Substitute the two genuine second moments and the actual reflection-block norm defect for Pg=g. The same S therefore supplies the microscopic block norm-square.

\[\int\operatorname{Var}_{S_y}(f)d\nu=\int f^2d\nu-\int(Tf)^2d\nu=\|g\|^2-\|Ag\|^2=\|Bg\|^2.\]

Corresponding Lean step

hvar; hgn; hAgn; hblock g hPg; hvariance

7. Join the exact smooth gradient bound

Substitute the genuine variance/block identity into the already proved sharp smooth energy estimate. Every domain and the actual Bg are now internal outputs. This is the smooth compact block input used toward B.13; it does not construct Γ or extend the gradient operator to arbitrary rough L² classes.

\[\eta\int\|\nabla Tf\|^2d\nu\le\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}\left(\int f^2d\nu-\int(Tf)^2d\nu\right)=\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}\|Bg\|^2.\]

Corresponding Lean step

hbound; hvar; hvariance

8. Exercise zero energy and a noncentered class

At V=‖x‖²/2 and α=β=η=1, the sharp coefficient is zero and the actual smooth gradient energy vanishes. In rank zero the constant f=1 is smooth with compact support: its genuine class has norm-square one, Ag=g, and microscopic block/conditional variance/gradient energy zero. This verifies that no hidden centering premise entered the class or norm bridge.

\[\alpha=\beta=\eta=1\Rightarrow\int\|\nabla Tf\|^2d\nu=0;\qquad d=0,\ f=1\Rightarrow\|g\|^2=1,\ Ag=g,\ \|Bg\|^2=0.\]

Corresponding Lean step

Tests.ProximalBPSMacroscopicEnergy.gaussian_precision_macroscopic_energy; rank_zero_noncentered_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_gradient_energy_blocks

Keep one genuine conditional kernel and literal smooth mean; Produce the actual reflected-pair disintegration; Use AE uniqueness only for conditional means and classes; Identify the actual reflection operators and retain block algebra; Identify both actual second moments; Close the genuine microscopic variance identity; Join the exact smooth gradient bound; Exercise zero energy and a noncentered class

Download module (.lean)

theorem actual_macroscopic_gradient_energy_blocks
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E,
      (α : ℝ) * ‖a‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x a) a ∧
      (fderiv ℝ (fderiv ℝ V) x a) a ≤ (β : ℝ) * ‖a‖^2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    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 ν ∧
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2 : ℝ) • x - y)) ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun u => -V ((1/2 : ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
      Λ.IsCondKernel S ∧ Λ.fst = ν ∧
      ∃ U : Lp ℝ 2 J →ₗᵢ[ℝ] Lp ℝ 2 J,
        (∀ g : Lp ℝ 2 J, (U g : E × E → ℝ) =ᵐ[J] g ∘ F) ∧
        Function.Involutive U ∧ IsSelfAdjoint U.toContinuousLinearMap ∧
        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) ∧
        (∀ g : Lp ℝ 2 J, P g = g → ‖B g‖^2 = ‖g‖^2 - ‖A g‖^2) ∧
        ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
          let Tf := fun y => ∫ u, f u ∂S y
          Differentiable ℝ Tf ∧ MemLp f 2 ν ∧ MemLp Tf 2 ν ∧
          MemLp (gradient Tf) 2 ν ∧
          Integrable (fun y =>
            AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
              (S y) f) ν ∧
          ∃ g : Lp ℝ 2 J,
            (g : E × E → ℝ) =ᵐ[J] (fun p => f p.2) ∧ P g = g ∧
            (A g : E × E → ℝ) =ᵐ[J] (fun p => Tf p.2) ∧
            ‖g‖^2 = (∫ y, (f y)^2 ∂ν) ∧
            ‖A g‖^2 = (∫ y, (Tf y)^2 ∂ν) ∧
            (∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
              (S y) f ∂ν) = ‖B g‖^2 ∧
            η * (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤
              (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) * ‖B g‖^2 := by
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    (μ.prod (stdGaussian E))
  let ν := J.snd
  let Λ := J.map (fun p : E × E => (p.2,(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,hcond,hSR,hSd,henergy⟩ :=
    ConditionalGradientEnergy.reflected_conditional_gradient_energy hα hαβ hV hH hη hβη
  let : IsProbabilityMeasure μ := hμ
  let : IsProbabilityMeasure J := hJ
  let : IsProbabilityMeasure ν := hν
  let : IsMarkovKernel R := hR
  let : IsMarkovKernel S := hS
  let : (J.map Prod.swap).IsCondKernel R := hcond

  -- Transform the actual disintegration, not an independently chosen law.
  let G := fun p : E × E => (p.1,(2:ℝ) • p.2-p.1)
  have hG : Measurable G := by fun_prop
  have hmap : (J.map Prod.swap).fst ⊗ₘ S =
      ((J.map Prod.swap).fst ⊗ₘ R).map G := by
    ext t ht
    rw [Measure.compProd_apply ht, Measure.map_apply hG ht,
      Measure.compProd_apply (hG ht)]
    apply lintegral_congr_ae
    filter_upwards with y
    rw [hSR y, Measure.map_apply (by fun_prop) (measurable_prodMk_left ht)]
    rfl
  have hΛmap : (J.map Prod.swap).map G = Λ := by
    rw [Measure.map_map hG (by fun_prop)]
    rfl
  have hfst : Λ.fst = ν := by
    rw [← hΛmap, Measure.fst_map_prodMk (by fun_prop)]
    change (J.map Prod.swap).fst = ν
    exact Measure.fst_map_swap
  have hΛcond : Λ.IsCondKernel S := by
    constructor
    rw [hfst, show ν = (J.map Prod.swap).fst from Measure.fst_map_swap.symm,
      hmap, Measure.disintegrate (J.map Prod.swap) R, hΛmap]
  let : Λ.IsCondKernel S := hΛcond

  obtain ⟨S₀,hS₀,hΛ₀,hfst₀,U₀,hU₀,hUi₀,hUs₀,hrep₀⟩ :=
    MacroscopicRepresentative.macroscopic_reflection_smooth_representative hα hV hH hη
  let : IsMarkovKernel S₀ := hS₀
  let : Λ.IsCondKernel S₀ := hΛ₀
  have hκ : S =ᵐ[ν] S₀ := by
    have h₁ : S =ᵐ[Λ.fst] Λ.condKernel :=
      eq_condKernel_of_measure_eq_compProd S (Measure.disintegrate Λ S).symm
    have h₀ : S₀ =ᵐ[Λ.fst] Λ.condKernel :=
      eq_condKernel_of_measure_eq_compProd S₀ (Measure.disintegrate Λ S₀).symm
    have hk : S =ᵐ[Λ.fst] S₀ := h₁.trans h₀.symm
    simpa only [hfst] using hk
  have hκJ : ∀ᵐ p ∂J, S p.2 = S₀ p.2 :=
    ae_of_ae_map measurable_snd.aemeasurable hκ

  obtain ⟨R₁,hR₁,hRf₁,U,hU,hUi,hUs,hRp,hBB,hBD,hblock⟩ :=
    ReflectionL2.actual_reflection_block_identities μ hη
  have hUU : U₀ = U := by
    apply LinearIsometry.ext
    intro g
    exact Lp.ext ((hU₀ g).trans (hU g).symm)
  refine ⟨hμ,hJ,hν,R,S,hR,hS,hcond,hSR,hSd,hΛcond,hfst,U,hU,hUi,hUs,
    hBB,hBD,hblock,?_⟩
  intro f hf hfc
  let Tf := fun y => ∫ u, f u ∂S y
  obtain ⟨hd,hf2,hTf2,hgrad2,hvarI,hvar,hbound⟩ := henergy f hf hfc
  obtain ⟨g,hg,hPg,hAg,hTf₀2,hscore⟩ := hrep₀ f hf hfc
  rw [hUU] at hAg
  let A := P * U.toContinuousLinearMap * P
  let B := (1-P) * U.toContinuousLinearMap * P
  have hAgS : (A g : E × E → ℝ) =ᵐ[J] (fun p => Tf p.2) := by
    apply hAg.trans
    filter_upwards [hκJ] with p hp
    change (∫ u, f u ∂S₀ p.2) = ∫ u, f u ∂S p.2
    rw [hp]

  -- A joint representative's actual second moment uses the actual snd law.
  have norm_snd (v : Lp ℝ 2 J) (φ : E → ℝ) (hφ : Continuous φ)
      (hv : (v : E × E → ℝ) =ᵐ[J] (fun p => φ p.2)) :
      ‖v‖^2 = ∫ y, (φ y)^2 ∂ν := by
    calc
      ‖v‖^2 = ∫ p, (φ p.2)^2 ∂J := by
        rw [← real_inner_self_eq_norm_sq, L2.inner_def]
        apply integral_congr_ae
        filter_upwards [hv] with p hp
        rw [hp]
        simp [pow_two]
      _ = ∫ y, (φ y)^2 ∂ν :=
        (integral_map measurable_snd.aemeasurable
          (hφ.pow 2).aestronglyMeasurable).symm
  have hgn := norm_snd g f hf.continuous hg
  have hAgn := norm_snd (A g) Tf hd.continuous hAgS
  have hvariance : (∫ y,
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
        (S y) f ∂ν) = ‖B g‖^2 := by
    calc
      _ = ‖g‖^2-‖A g‖^2 := by rw [hvar,hgn,hAgn]
      _ = ‖B g‖^2 := (hblock g hPg).symm
  refine ⟨hd,hf2,hTf2,hgrad2,hvarI,g,hg,hPg,hAgS,hgn,hAgn,hvariance,?_⟩
  calc
    η * (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤
        (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) *
          ((∫ y, (f y)^2 ∂ν)-(∫ y, (Tf y)^2 ∂ν)) := hbound
    _ = (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) * ‖B g‖^2 := by
      rw [← hvar,hvariance]

end AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source Euclidean C² Hessian and positive-step/cap assumptions.	Finite real Hilbert/Borel space including rank zero, with unchanged genuine curvature and step premises.	generalization	Authored finite-Hilbert/rank-zero extension; no added law/domain/operator certificate.
B.9 true microscopic variance norm and C.2 smooth gradient energy for actual compressed reflection.	Same actual J, ν, Λ, S, P, U and g with genuine second moments and exact coefficient; A/B/D are authored aliases.	same	Internally produced disintegration, AE class identification and true norm/moment bookkeeping; AE kernel agreement never transports derivatives.
Full rough B.13 gradient-domain/Γ, half-turn and full sampler/cost results.	Actual joint L2 block and smooth compact energy integration, SAME law/kernels/operators and classical integral representative; actual variance equals microscopic block norm-square. Full rough L2-H1/outer closed-gradient/Gamma/half-turn/main/implementation error/expected costs/composition remain separate. Focused build passed3891; independent wholeproof/blind/source/exactcommit/shared admission pending.	unresolved	No rough L²-H¹ extension, operator positive root, nonexplosion/convergence/error/query cost or actual-input composition is proved by this smooth block join.

Actual joint L2 block and smooth compact energy integration, SAME law/kernels/operators and classical integral representative; actual variance equals microscopic block norm-square. Full rough L2-H1/outer closed-gradient/Gamma/half-turn/main/implementation error/expected costs/composition remain separate. Focused build passed3891; independent wholeproof/blind/source/exactcommit/shared admission pending.

Encoder–denoiser: accepted · equivalent-after-elaboration

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 joint L2 block and smooth compact energy integration, SAME law/kernels/operators and classical integral representative; actual variance equals microscopic block norm-square. Full rough L2-H1/outer closed-gradient/Gamma/half-turn/main/implementation error/expected costs/composition remain separate. Focused build passed3891; independent wholeproof/blind/source/exactcommit/shared admission pending.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.compProd_apply
MeasureTheory.Measure.map_apply
MeasureTheory.Measure.map_map
MeasureTheory.Measure.fst_map_prodMk
MeasureTheory.Measure.fst_map_swap
MeasureTheory.Measure.disintegrate
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
MeasureTheory.ae_of_ae_map
LinearIsometry.ext
MeasureTheory.Lp.ext
MeasureTheory.L2.inner_def
real_inner_self_eq_norm_sq
MeasureTheory.integral_congr_ae
MeasureTheory.integral_map

Mathematical sources

Fixed PBPS arXiv2609.06905v1 B.1-B.9 actual conditional projection/reflection compression and variance defect; C.1 formula(C.2) smooth compact energy. B.13 rough-domain and B.10-B.11 Gamma excluded. — Actual joint L2 block and smooth compact energy integration, SAME law/kernels/operators and classical integral representative; actual variance equals microscopic block norm-square. Full rough L2-H1/outer closed-gradient/Gamma/half-turn/main/implementation error/expected costs/composition remain separate. Focused build passed3891; independent wholeproof/blind/source/exactcommit/shared admission pending.

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

Actual macroscopic reflection blocks and sharp smooth gradient energy

Complete source statement (Samplinglib restatement)

Actual macroscopic reflection blocks and sharp smooth gradient energy

Read the formalized proofs

Actual macroscopic reflection blocks and sharp smooth gradient energy

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Keep one genuine conditional kernel and literal smooth mean

2. Produce the actual reflected-pair disintegration

3. Use AE uniqueness only for conditional means and classes

4. Identify the actual reflection operators and retain block algebra

5. Identify both actual second moments

6. Close the genuine microscopic variance identity

7. Join the exact smooth gradient bound

8. Exercise zero energy and a noncentered class

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?