Samplinglib mathematical lesson

Exact centered squared-defect coercivity and bounded inverse

Tests.ProximalBPSCenteredDefect.actual_centered_defect_coercive_and_unit · theorem · Teaching coverage

Read this first

Mathematical statement

E is a finite-dimensional real Hilbert Borel space with canonical volume; rank zero is an explicit extension of the source Euclidean convention. V:E→ℝ is C²; 0<α≤β; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0 and βη≤1. μ=volume.tilted(−V), J=Law(X,X+√ηZ) for independent X∼μ and Z∼N(0,I), and ν=J.snd. Finite dimensionality of E does not imply finite dimensionality of L²(ν). There exist a selfadjoint bounded operator T on L²(ν) with the literal ν-a.e. action Tu(y)=∫u(x)S(y,dx), where S(y)=volume.tilted(x↦−V((y+x)/2)−‖y−x‖²/(8η)); a class q=1 ν-a.e. with ⟨q,u⟩=∫u dν for all u; and the actual selfadjoint restriction T₀ to H₀=ker⟨q,·⟩. Set ρ=(1−αη)/(1+αη) and δ=4αη/(1+αη)². The squared defect D₀=I_H₀−T₀² is positive. For every u∈H₀, T₀u=Tu as an ambient class, ‖T₀u‖≤ρ‖u‖, ⟨D₀u,u⟩=‖u‖²−‖T₀u‖² and δ‖u‖²≤⟨D₀u,u⟩. D₀ is a unit in the algebra of bounded continuous linear endomorphisms of H₀; hence it has a bounded inverse on this exact centered space. The original hypotheses force δ>0 and include αη=1. No full-space inverse or positive square root is claimed.

\[\rho=\frac{1-\alpha\eta}{1+\alpha\eta},\quad\delta=\frac{4\alpha\eta}{(1+\alpha\eta)^2}>0,\quad\|T_0u\|\le\rho\|u\|,\quad\langle D_0u,u\rangle\ge\delta\|u\|^2,\quad D_0\in\operatorname{GL}(H_0).\]

Lean statement · actual_centered_defect_coercive_and_unit

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_defect_coercive_and_unit
    {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 ν := J.snd
    ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
      IsSelfAdjoint T ∧
      (∀ u : Lp ℝ 2 ν, (T u : E → ℝ) =ᵐ[ν]
        (fun y => ∫ x, u x ∂((volume : Measure E).tilted
          (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))))) ∧
      ∃ q : Lp ℝ 2 ν,
        (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧
        (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
        ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
          (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
          IsSelfAdjoint T0 ∧ ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
          (∀ u : ((innerSL ℝ q).ker),
            ‖T0 u‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ ∧
            inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2 ∧
            (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖u‖^2 ≤
              inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u) ∧
          IsUnit ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0)

Exact module and namespace context

Proof roadmap

1Use the same actual reflection and actual pullback
Compare the AE reflection actions to identify the operator U in the verified macroscopic contraction. For the actual M from the producer, PM=M gives macro-range membership. Its AE action Mu(x,y)=u(y) and the actual marginal ν=J.snd give mean transport directly, so centered u yields a centered macro input. No extra onto witness or copied Poincare proof is needed.
2Transport the exact sharp contraction
Apply the verified sharp macro contraction to Mu. The actual identity MT=PUPM and the isometry transfer the constant without changing laws or operators.
3Derive the positive coercivity constant
Square the contraction and use the actual quadratic defect identity. Since 0<αη≤1, the exact scalar identity yields a strictly positive lower bound, including the endpoint αη=1.
4Obtain a bounded inverse on the centered space
The centered kernel is a complete Hilbert space because it is closed in L². Apply the fixed Mathlib coercivity-to-unit theorem to D₀ with δ. IsUnit means that an inverse exists in the algebra of bounded continuous linear endomorphisms of this same centered space. In the norm hypothesis, nonnegativity of the quadratic form follows directly from the already proved δ gap.

Full assumptions and notation

All objects and hypotheses

The complete potential, curvature, initialization law and step conditions are stated above. No operator, probability, stationarity, mean-zero preservation or coercivity certificate is supplied by the caller.
L² consists of AE classes; finite dimension of E does not make L² finite dimensional. The whole closed mean-zero subspace is used.
Zero-dimensional E is explicitly included as an extension of the source Euclidean convention; αη=1 is retained.

Mathematical proof

1. Use the same actual reflection and actual pullback

Compare the AE reflection actions to identify the operator U in the verified macroscopic contraction. For the actual M from the producer, PM=M gives macro-range membership. Its AE action Mu(x,y)=u(y) and the actual marginal ν=J.snd give mean transport directly, so centered u yields a centered macro input. No extra onto witness or copied Poincare proof is needed.

\[PMu=Mu,\quad\int Mu\,dJ=\int u\,d\nu=0.\]

Corresponding Lean step

hSameU; hAll; hM; integral_congr_ae; integral_map

2. Transport the exact sharp contraction

Apply the verified sharp macro contraction to Mu. The actual identity MT=PUPM and the isometry transfer the constant without changing laws or operators.

\[\|T_0u\|\le\rho\|u\|,\quad\rho=\frac{1-\alpha\eta}{1+\alpha\eta}\in[0,1).\]

Corresponding Lean step

hSharp; hCon; M.norm_map; hT0

3. Derive the positive coercivity constant

Square the contraction and use the actual quadratic defect identity. Since 0<αη≤1, the exact scalar identity yields a strictly positive lower bound, including the endpoint αη=1.

\[\delta=1-\rho^2=\frac{4\alpha\eta}{(1+\alpha\eta)^2}>0,\quad\delta\|u\|^2\le\langle D_0u,u\rangle.\]

Corresponding Lean step

hδ; hρ; hDef0; hGap; field_simp; ring

4. Obtain a bounded inverse on the centered space

The centered kernel is a complete Hilbert space because it is closed in L². Apply the fixed Mathlib coercivity-to-unit theorem to D₀ with δ. IsUnit means that an inverse exists in the algebra of bounded continuous linear endomorphisms of this same centered space. In the norm hypothesis, nonnegativity of the quadratic form follows directly from the already proved δ gap.

\[D_0=I_{H_0}-T_0^2\in\operatorname{GL}(H_0).\]

Corresponding Lean step

ContinuousLinearMap.completeSpace_ker; isUnit_of_forall_le_norm_inner_map; hUnit

Lean verification

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

Lean proof · actual_centered_defect_coercive_and_unit

Use the same actual reflection and actual pullback; Transport the exact sharp contraction; Derive the positive coercivity constant; Obtain a bounded inverse on the centered space

Download module (.lean)

theorem actual_centered_defect_coercive_and_unit
    {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 ν := J.snd
    ∃ T : Lp ℝ 2 ν →L[ℝ] Lp ℝ 2 ν,
      IsSelfAdjoint T ∧
      (∀ u : Lp ℝ 2 ν, (T u : E → ℝ) =ᵐ[ν]
        (fun y => ∫ x, u x ∂((volume : Measure E).tilted
          (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η))))) ∧
      ∃ q : Lp ℝ 2 ν,
        (q : E → ℝ) =ᵐ[ν] (fun _ => (1 : ℝ)) ∧
        (∀ u : Lp ℝ 2 ν, inner ℝ q u = ∫ y, u y ∂ν) ∧
        ∃ T0 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker),
          (∀ u : ((innerSL ℝ q).ker), (T0 u : Lp ℝ 2 ν) = T u) ∧
          IsSelfAdjoint T0 ∧ ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0).IsPositive ∧
          (∀ u : ((innerSL ℝ q).ker),
            ‖T0 u‖ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ ∧
            inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u = ‖u‖^2-‖T0 u‖^2 ∧
            (4*(α : ℝ)*η/(1+(α : ℝ)*η)^2)*‖u‖^2 ≤
              inner ℝ (((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) u) u) ∧
          IsUnit ((1 : ((innerSL ℝ q).ker) →L[ℝ] ((innerSL ℝ q).ker))-T0*T0) := 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 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,M,hM,T,hTs,hAll,
    q,hq,hTq,hPair,hH0,hD,hDq,hDef,T0,hT0,hT0s,hT0n,hD0,hD0sub,hDef0⟩ :=
    CenteredDefectOperator.actual_centered_selfadjoint_defect hα hαβ hV hH hη hβη
  letI : IsProbabilityMeasure J := hJ
  letI : IsProbabilityMeasure ν := hν
  let H0 : Submodule ℝ (Lp ℝ 2 ν) := (innerSL ℝ q).ker
  have hLiteral (u : Lp ℝ 2 ν) : (T u : E → ℝ) =ᵐ[ν]
      (fun y => ∫ x, u x ∂((volume : Measure E).tilted
        (fun x => -V ((1/2 : ℝ) • (y+x)) - ‖y-x‖^2/(8*η)))) := by
    filter_upwards [(hAll u).2.2.2.1] with y hy
    exact hy.trans (congrArg (fun m : Measure E => ∫ x, u x ∂m) (hSd y))
  have h58 := ProximalBPSMacroscopicRange.actual_centered_macro_contraction_and_defect_gap
    (E:=E) (V:=V) (α:=α) (β:=β) (η:=η) hα hαβ hV hH hη hβη
  dsimp only at h58
  obtain ⟨U58,hU58,hUi58,hUs58,hSharp⟩ := h58
  have hSameU : U58=U := LinearIsometry.ext (fun f =>
    Lp.ext ((hU58 f).trans (hU f).symm))
  subst U58
  have hCon (u : H0) : ‖T0 u‖ ≤
      ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ := by
    have hu : (∫ y, (u : Lp ℝ 2 ν) y ∂ν)=0 := (hH0 _).mp u.property
    have hr : M (u : Lp ℝ 2 ν) ∈ P.toLinearMap.range :=
      ⟨M u,(hAll (u : Lp ℝ 2 ν)).1⟩
    have hc : (∫ p, (M (u : Lp ℝ 2 ν)) p ∂J)=0 := by
      calc
        (∫ p, (M (u : Lp ℝ 2 ν)) p ∂J) = ∫ p : E × E, (u : Lp ℝ 2 ν) p.2 ∂J :=
          integral_congr_ae (hM (u : Lp ℝ 2 ν))
        _ = ∫ y, (u : Lp ℝ 2 ν) y ∂ν :=
          (integral_map (μ:=J) measurable_snd.aemeasurable
            (Lp.stronglyMeasurable (u : Lp ℝ 2 ν)).aestronglyMeasurable).symm
        _ = 0 := hu
    calc
      ‖T0 u‖ = ‖(T0 u : Lp ℝ 2 ν)‖ := rfl
      _ = ‖T (u : Lp ℝ 2 ν)‖ := congrArg norm (hT0 u)
      _ = ‖M (T (u : Lp ℝ 2 ν))‖ := (M.norm_map _).symm
      _ = ‖(P * U.toContinuousLinearMap * P) (M (u : Lp ℝ 2 ν))‖ :=
        congrArg norm ((hAll (u : Lp ℝ 2 ν)).2.1)
      _ ≤ ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖M (u : Lp ℝ 2 ν)‖ :=
        (hSharp (M (u : Lp ℝ 2 ν)) hr hc).1
      _ = ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖ :=
        congrArg (fun r : ℝ => ((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*r) (M.norm_map _)
  let δ : ℝ := 4*(α : ℝ)*η/(1+(α : ℝ)*η)^2
  have ha0 : 0 < (α : ℝ)*η := mul_pos hα hη
  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 hδ : 0 < δ := by dsimp [δ]; positivity
  have hGap (u : H0) : δ*‖u‖^2 ≤ inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u := by
    have hs : ‖T0 u‖^2 ≤ (((1-(α : ℝ)*η)/(1+(α : ℝ)*η))*‖u‖)^2 :=
      (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hρ (norm_nonneg _))).mpr (hCon u)
    have hr : δ = 1-((1-(α : ℝ)*η)/(1+(α : ℝ)*η))^2 := by
      dsimp [δ]
      field_simp [ne_of_gt hd]
      ring
    rw [hDef0,hr]
    nlinarith [hs]
  have hUnit : IsUnit ((1 : H0 →L[ℝ] H0)-T0*T0) := by
    apply ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map
      ((1 : H0 →L[ℝ] H0)-T0*T0) (c:=⟨δ,hδ.le⟩) (by exact hδ)
    intro u
    change ‖u‖^2*δ ≤ ‖inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u‖
    have hnn : 0 ≤ inner ℝ (((1 : H0 →L[ℝ] H0)-T0*T0) u) u :=
      (mul_nonneg hδ.le (sq_nonneg ‖u‖)).trans (hGap u)
    rw [Real.norm_eq_abs,abs_of_nonneg hnn,mul_comm]
    exact hGap u
  refine ⟨T,hTs,hLiteral,q,hq,hPair,T0,hT0,hT0s,hD0,?_,hUnit⟩
  intro u
  exact ⟨hCon u,hDef0 u,hGap u⟩

end
end Tests.ProximalBPSCenteredDefect

#print axioms Tests.ProximalBPSCenteredDefect.actual_centered_defect_coercive_and_unit

Exact module and namespace context

Scope and omitted-condition boundaries

SAME actual55 T on L2(nu), selfadjoint/mean preserving/constant fixed, exact complete mean-zero restriction T0, full and centered positive squared defects; real Test uses actual58 rho/delta to prove IsUnit centered squared defect. No Gamma/root/polar/full weakH1/hypocoercivity/dynamics/main/implementation error/cost/composition/fullpaper/Goal admission.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

LinearIsometry.ext
Lp.ext
integral_congr_ae
integral_map
LinearIsometry.norm_map
sq_le_sq₀
ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map

Mathematical sources

PBPS2609.06905v1 AppendixB B1-B5, D1-D2 real L2 stationarity/centering, C4/B15 squared-defect precursor; exact31regions/54items source inventory independently covered. — SAME actual55 T on L2(nu), selfadjoint/mean preserving/constant fixed, exact complete mean-zero restriction T0, full and centered positive squared defects; real Test uses actual58 rho/delta to prove IsUnit centered squared defect. No Gamma/root/polar/full weakH1/hypocoercivity/dynamics/main/implementation error/cost/composition/fullpaper/Goal admission.

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