Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
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.