Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

ProximalBPSMacroscopicRange: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Sharp contraction and defect gap for every centered macro input
Samplinglib mathematical lesson

Sharp contraction and defect gap for every centered macro input

Tests.ProximalBPSMacroscopicRange.actual_centered_macro_contraction_and_defect_gap · theorem · Teaching coverage

Read this first

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). There exists one linear isometry U:L²(J)→L²(J) whose AE representative is composition with F(x,y)=(x,2x−y), with U²=I and U self-adjoint. Define A=PUP and B=(I−P)UP. For every f∈ran P with ∫f dJ=0, ‖Af‖≤[(1−αη)/(1+αη)]‖f‖ and [4αη/(1+αη)²]‖f‖²≤‖Bf‖². This includes αη=1, uses the actual, potentially infinite-dimensional L²(J), without imposing finite-dimensionality on L², and is Test-level integration of already produced operators; Γ, its inverse and trajectories are not asserted.

\[\rho=\frac{1-\alpha\eta}{1+\alpha\eta},\quad\|Af\|\le\rho\|f\|,\quad\|Bf\|^2\ge\frac{4\alpha\eta}{(1+\alpha\eta)^2}\|f\|^2\quad(f\in\operatorname{ran}P\cap L^2_0(J)).\]
Lean statement · actual_centered_macro_contraction_and_defect_gap

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). There exists one linear isometry U:L²(J)→L²(J) whose AE representative is composition with F(x,y)=(x,2x−y), with U²=I and U self-adjoint. Define A=PUP and B=(I−P)UP. For every f∈ran P with ∫f dJ=0, ‖Af‖≤[(1−αη)/(1+αη)]‖f‖ and [4αη/(1+αη)²]‖f‖²≤‖Bf‖². This includes αη=1, uses the actual, potentially infinite-dimensional L²(J), without imposing finite-dimensionality on L², and is Test-level integration of already produced operators; Γ, its inverse and trajectories are not asserted.

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_centered_macro_contraction_and_defect_gap
    {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 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
    ∃ 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
      ∀ f : Lp ℝ 2 J, f ∈ P.toLinearMap.range → (∫ p, f p ∂J)=0 →
        ‖A f‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖f‖ ∧
        (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖f‖^2 ≤ ‖B f‖^2

Exact module and namespace context

Proof roadmap

  1. 1Match the actual previously produced operators

    The actual reflection/mean theorem produces U,M55,T55 and its defect identity. AE canonical pullback shows M55=M. AE equality to the same literal reflected kernel S, whose every-y density is produced internally, gives T55=T57 for the already verified sharp scalar contraction operator.

  2. 2Lift scalar contraction to every macro input

    The new full centered image produces centered u with Mu=f for every centered f in ranP. Apply the verified exact scalar contraction to this same T55, then use MT55=AM and isometry of M. No caller image or output-centering certificate is used.

  3. 3Derive the sharp squared defect gap

    The actual orthogonal norm defect is ‖BMu‖²=‖u‖²−‖Tu‖². Original α≤β and βη≤1 imply 0≤αη≤1 and ρ≥0, so the norm contraction can be squared. Subtraction and exact scalar algebra give 1−ρ²=4αη/(1+αη)², without division by 1−αη.

  4. 4Keep the operator-root boundary explicit

    The consumer proves a squared B lower bound in a Test module for all true centered macro inputs. It does not construct the positive real-Hilbert root Γ=(B*B)^(1/2), a centered inverse, source weak-H1 equivalence, half-turn mixing, implementation errors or oracle cost.

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. Match the actual previously produced operators

The actual reflection/mean theorem produces U,M55,T55 and its defect identity. AE canonical pullback shows M55=M. AE equality to the same literal reflected kernel S, whose every-y density is produced internally, gives T55=T57 for the already verified sharp scalar contraction operator.

\[M_{55}=M,\quad T_{55}=T_{57},\quad MT_{55}=AM.\]
Corresponding Lean step

L2MacroscopicMean.actual_macroscopic_l2_mean; hSameM; hSd; hLaw; hSameT; Tests.GaussianMarginalPoincare.actual_same_mean_centered_contraction

2. Lift scalar contraction to every macro input

The new full centered image produces centered u with Mu=f for every centered f in ranP. Apply the verified exact scalar contraction to this same T55, then use MT55=AM and isometry of M. No caller image or output-centering certificate is used.

\[f=Mu,\quad\|Af\|=\|MTu\|=\|Tu\|\le\rho\|u\|=\rho\|f\|.\]
Corresponding Lean step

MacroscopicRange.actual_macroscopic_centered_range; hCentered; hCon; hMT; M.norm_map

3. Derive the sharp squared defect gap

The actual orthogonal norm defect is ‖BMu‖²=‖u‖²−‖Tu‖². Original α≤β and βη≤1 imply 0≤αη≤1 and ρ≥0, so the norm contraction can be squared. Subtraction and exact scalar algebra give 1−ρ²=4αη/(1+αη)², without division by 1−αη.

\[\|Bf\|^2=\|u\|^2-\|Tu\|^2\ge(1-\rho^2)\|u\|^2=\frac{4\alpha\eta}{(1+\alpha\eta)^2}\|f\|^2.\]
Corresponding Lean step

hDef; ha1; hρ; sq_le_sq₀; hr; field_simp; ring; nlinarith

4. Keep the operator-root boundary explicit

The consumer proves a squared B lower bound in a Test module for all true centered macro inputs. It does not construct the positive real-Hilbert root Γ=(B*B)^(1/2), a centered inverse, source weak-H1 equivalence, half-turn mixing, implementation errors or oracle cost.

\[\text{Squared defect bound}\quad\not\Rightarrow\quad\text{an already constructed }\Gamma^{-1}.\]
Corresponding Lean step

No Gamma/root/inverse declaration is present.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_centered_macro_contraction_and_defect_gap

Match the actual previously produced operators; Lift scalar contraction to every macro input; Derive the sharp squared defect gap; Keep the operator-root boundary explicit

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_centered_macro_contraction_and_defect_gap
    {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 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
    ∃ 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
      ∀ f : Lp ℝ 2 J, f ∈ P.toLinearMap.range → (∫ p, f p ∂J)=0 →
        ‖A f‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖f‖ ∧
        (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖f‖^2 ≤ ‖B f‖^2 := 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 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ν,S,hS,hSd,hSc,hSf,hSs,U,hU,hUi,hUs,M55,hM55,T55,hAll⟩ :=
    L2MacroscopicMean.actual_macroscopic_l2_mean hα hαβ hV hH hη hβη
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  have hSameM : M55=M := LinearIsometry.ext (fun u =>
    Lp.ext ((hM55 u).trans (Lp.coeFn_compMeasurePreserving u hp).symm))
  subst M55
  obtain ⟨_,_,hRange,hMean,hCentered⟩ :=
    MacroscopicRange.actual_macroscopic_centered_range hα hαβ hV hH hη hβη
  obtain ⟨G,hClose,hClosed,T57,K,h57⟩ :=
    Tests.GaussianMarginalPoincare.actual_same_mean_centered_contraction hα hαβ hV hH hη hβη
  have hSameT (u : Lp ℝ 2 ν) : T55 u=T57 u := by
    rcases hAll u with ⟨_,_,_,hTa,_,_,_,_⟩
    rcases h57 u with ⟨_,hTb,_,_⟩
    apply Lp.ext
    have hLaw : (fun y : E => ∫ x, u x ∂S y) =ᵐ[ν]
        (fun y => ∫ x, u x ∂((volume : Measure E).tilted
          (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η)))) :=
      Filter.Eventually.of_forall (fun y =>
        congrArg (fun m : Measure E => ∫ x, u x ∂m) (hSd y))
    exact hTa.trans (hLaw.trans hTb.symm)
  refine ⟨U,hU,hUi,hUs,?_⟩
  intro f hf hf0
  have hfimage : f ∈ M '' {u : Lp ℝ 2 ν | (∫ y, u y ∂ν)=0} := by
    rw [hCentered]
    exact ⟨hf,hf0⟩
  obtain ⟨u,hu,huf⟩ := hfimage
  subst f
  rcases hAll u with ⟨hPM,hMT,hTn,hTa,hFiber,hIv,hVar,hDef⟩
  rcases h57 u with ⟨hGraph,hT57,hMean57,hCn⟩
  have hCon : ‖T55 u‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ := by
    rw [hSameT u]
    exact (hCn hu).2
  constructor
  · calc
      ‖(P * U.toContinuousLinearMap * P) (M u)‖ = ‖M (T55 u)‖ :=
        congrArg norm hMT.symm
      _ = ‖T55 u‖ := M.norm_map _
      _ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ := hCon
      _ = ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖M u‖ := by rw [M.norm_map]
  · have ha0 : 0 ≤ (α : ℝ)*η := mul_nonneg hα.le hη.le
    have ha1 : (α : ℝ)*η ≤ 1 :=
      (mul_le_mul_of_nonneg_right (by exact_mod_cast hαβ) hη.le).trans hβη
    have hd : 0 < 1+(α : ℝ)*η := by positivity
    have hρ : 0 ≤ (1-(α : ℝ)*η)/(1+(α : ℝ)*η) :=
      div_nonneg (sub_nonneg.mpr ha1) hd.le
    have hs : ‖T55 u‖^2 ≤ (((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖)^2 :=
      (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hρ (norm_nonneg _))).mpr hCon
    have hr : 4*(α : ℝ)*η/(1+(α : ℝ)*η)^2 =
        1-((1-(α : ℝ)*η)/(1+(α : ℝ)*η))^2 := by
      field_simp [ne_of_gt hd]
      ring
    rw [M.norm_map,hDef,hr]
    nlinarith [hs]

end
end Tests.ProximalBPSMacroscopicRange

#print axioms AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange.l2_pullback_range_eq_lpMeas
#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange.actual_macroscopic_centered_range
#print axioms Tests.ProximalBPSMacroscopicRange.actual_centered_macro_contraction_and_defect_gap

Exact module and namespace context

Scope 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

Mathlib API called (external library)

  • LinearIsometry.ext
  • Lp.ext
  • LinearIsometry.norm_map
  • sq_le_sq₀

Mathematical sources

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