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

ConditionalGradientEnergy: 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 outer gradient energy for the actual reflected conditional mean
Samplinglib mathematical lesson

Sharp outer gradient energy for the actual reflected conditional mean

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientEnergy.reflected_conditional_gradient_energy · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C2 and 0<alpha≤beta with alpha||a||²≤D²V(x)[a,a]≤beta||a||² for every x,a. For eta>0 and beta*eta≤1, let mu be the literal normalized volume tilt exp(-V), J the actual law of (X,X+sqrt(eta)G) with independent X~mu and standard Gaussian G, and nu=J.snd. The theorem produces genuine probability of mu,J,nu and common Markov kernels R,S, with R disintegrating swappedJ, every-y S the pushforward of R by x→2x-y and the exact normalized density exp(-V((y+u)/2)-||y-u||²/(8eta)). For every signed globally smooth compactly supported f, Tf(y)=integral f dS(y) is globally differentiable, f,Tf and its true gradient belong to L2(nu), and the actual conditional variance is integrable under nu. Its outer integral equals integral f²dnu-integral(Tf)²dnu. Moreover eta integral||gradientTf||²dnu is at most (1-alphaeta)²/[4(1+alphaeta)] times that same defect. All probability, conditional-law and analytic domains are outputs; no centering of f or extra certificates are assumed.

\[\eta\int\|\nabla Tf\|^2\,d\nu\le\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}\left(\int f^2\,d\nu-\int(Tf)^2\,d\nu\right),\qquad\int\operatorname{Var}_{S_y}(f)\,d\nu(y)=\int f^2\,d\nu-\int(Tf)^2\,d\nu.\]
Lean statement · reflected_conditional_gradient_energy

Let E be a finite-dimensional real Hilbert space with its Borel structure, including rank zero. Let V be globally C2 and 0<alpha<=beta with alpha||a||²<=D²V(x)[a,a]<=beta||a||² for every x,a. For eta>0 and beta*eta<=1, let mu be the literal normalized volume tilt exp(-V), J the actual law of (X,X+sqrt(eta)G) with independent X~mu and standard Gaussian G, and nu=J.snd. The theorem produces genuine probability of mu,J,nu and common Markov kernels R,S, with R disintegrating swappedJ, every-y S the pushforward of R by x->2x-y and the exact normalized density exp(-V((y+u)/2)-||y-u||²/(8eta)). For every signed globally smooth compactly supported f, Tf(y)=integral f dS(y) is globally differentiable, f,Tf and its true gradient belong to L2(nu), and the actual conditional variance is integrable under nu. Its outer integral equals integral f²dnu-integral(Tf)²dnu. Moreover eta integral||gradientTf||²dnu is at most (1-alphaeta)²/[4(1+alphaeta)] times that same defect. All probability, conditional-law and analytic domains are outputs; no centering of f or extra certificates are assumed.

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 reflected_conditional_gradient_energy
    {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
    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*η))) ∧
      ∀ (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) ν ∧
        (∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
          (S y) f ∂ν) = (∫ y, (f y)^2 ∂ν) - (∫ y, (Tf y)^2 ∂ν) ∧
        η * (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤
          (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) *
            ((∫ y, (f y)^2 ∂ν) - (∫ y, (Tf y)^2 ∂ν))

Exact module and namespace context

Proof roadmap

  1. 1Produce genuine laws and one common conditional kernel

    The genuine Hessian/Gibbs parent gives a strictly positive normalizer and probability of the literal Gaussian augmentation. A nonintegrable exponential has totalized integral zero, contradicting that normalizer; therefore mu is genuinely normalized. Its joint second marginal nu is a probability. Reuse the already verified pointwise parent to obtain one R/S before all observations, including its every-y normalized reflected density.

  2. 2Retain all actual finite second-moment domains

    Compact continuity bounds |f| by a finite M. Every S_y and nu is an actual probability, so f lies in all required L2 spaces. Measurable kernel integration makes Tf and the conditional second moment strongly measurable; their bounds M and M² produce Tf L2 and conditional-second-moment L1 under nu. No analytic-domain certificate is supplied by the caller.

  3. 3Integrate through the same disintegration

    The actual conditional predicate gives nu compProd R=swappedJ. Push f² through the explicit reflected map in each fiber, then use Fubini with the bounded measurable joint integrand. This uses the very same R/S returned by the pointwise parent and does not identify unrelated conditional witnesses pointwise.

  4. 4Use actual Gaussian reflection invariance

    The genuine Gaussian parent fixes X and reflects the auxiliary Y about X; this joint pushforward preserves J. Applying the second-coordinate projection gives that the reflected second moment equals the original nu second moment. This is invariance of the augmentation law, not invariance or nonexplosion of a PBPS process.

  5. 5Produce the exact conditional variance defect

    On each actual probability fiber, its genuine L2 domain allows the centered-square variance identity. Integrability of both outer terms gives integrability of the actual variance and allows subtraction under the integral. Joint reflection identifies the first term, so the displayed defect is exact even for noncentered signed f.

  6. 6Derive the true outer gradient domain

    The pointwise parent proves actual differentiability of Tf. Mathlib measurable_fderiv followed by the continuous inverse Riesz map makes its true gradient strongly measurable. Its square is dominated by C_eta times the already integrable actual conditional variance, so it is integrable and the gradient lies in L2(nu). Fiber Poincare domains are not substituted for this outer domain.

  7. 7Integrate with the exact source coefficient

    All domains have now been produced. Integrate the pointwise inequality, multiply by positive eta, and simplify the genuine positive denominators. Substitute the exact variance-defect identity. The coefficient remains sharp, including its zero at alphaeta=1; no arbitrary energy premise is introduced.

  8. 8Consume the Gaussian precision and zero-dimensional boundaries

    For the actual quadratic potential V=||x||²/2 with alpha=beta=eta=1, the coefficient is zero. The actual gradient energy therefore vanishes, while global differentiability, all three L2 domains, variance L1 and its defect identity remain available. A separate fully stated Test specializes these actual laws and domains to rank zero.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real Hilbert/Borel E, includingrank0; this authored Euclidean generalization is explicit.
  • GlobalC2 potential V; 0<alpha≤beta with genuine Hessian lower/upper bounds alpha||a||²≤D²V(x)[a,a]≤beta||a||² for every x,a.
  • eta>0 with beta*eta≤1, exactly the source step restriction.
  • Signed globally smooth compactly supported observations f. Actualmu/J/nu probabilities, commontrueR/S and every-y density, differentiability/L2/varianceL1/defect are produced internally.

Mathematical proof

1. Produce genuine laws and one common conditional kernel

The genuine Hessian/Gibbs parent gives a strictly positive normalizer and probability of the literal Gaussian augmentation. A nonintegrable exponential has totalized integral zero, contradicting that normalizer; therefore mu is genuinely normalized. Its joint second marginal nu is a probability. Reuse the already verified pointwise parent to obtain one R/S before all observations, including its every-y normalized reflected density.

\[Z_V=\int e^{-V}dx>0,\quad\mu(dx)=Z_V^{-1}e^{-V(x)}dx,\quad J=\mathcal L(X,X+\sqrt\eta G),\quad\nu=J_\mathrm{snd}.\]
Corresponding Lean step

GibbsAugmentation.normalized_augmentation_density; integral_undef; isProbabilityMeasure_tilted; ConditionalGradientVariance.reflected_conditional_gradient_variance; hcond; hSR; hSd

2. Retain all actual finite second-moment domains

Compact continuity bounds |f| by a finite M. Every S_y and nu is an actual probability, so f lies in all required L2 spaces. Measurable kernel integration makes Tf and the conditional second moment strongly measurable; their bounds M and M² produce Tf L2 and conditional-second-moment L1 under nu. No analytic-domain certificate is supplied by the caller.

\[|f|\le M,\quad|Tf(y)|\le M,\quad f\in L^2(\nu)\cap L^2(S_y),\quad Tf\in L^2(\nu).\]
Corresponding Lean step

MemLp.of_bound; StronglyMeasurable.integral_kernel; norm_integral_le_of_norm_le_const; hfy2; hTf2; hfsqI

3. Integrate through the same disintegration

The actual conditional predicate gives nu compProd R=swappedJ. Push f² through the explicit reflected map in each fiber, then use Fubini with the bounded measurable joint integrand. This uses the very same R/S returned by the pointwise parent and does not identify unrelated conditional witnesses pointwise.

\[\int\!\int f(u)^2 S_y(du)\,\nu(dy)=\int f(2x-y)^2 J(dx,dy).\]
Corresponding Lean step

reflected_second_moment; IsCondKernel.disintegrate; integral_map_of_stronglyMeasurable; Measure.integral_compProd; Measure.fst_map_swap

4. Use actual Gaussian reflection invariance

The genuine Gaussian parent fixes X and reflects the auxiliary Y about X; this joint pushforward preserves J. Applying the second-coordinate projection gives that the reflected second moment equals the original nu second moment. This is invariance of the augmentation law, not invariance or nonexplosion of a PBPS process.

\[\mathcal R(x,y)=(x,2x-y),\quad\mathcal R_\#J=J\Longrightarrow\int f(2x-y)^2\,dJ=\int f^2\,d\nu.\]
Corresponding Lean step

GaussianReflection.reflection_preserves_augmentation; integral_map_of_stronglyMeasurable; reflected_second_moment

5. Produce the exact conditional variance defect

On each actual probability fiber, its genuine L2 domain allows the centered-square variance identity. Integrability of both outer terms gives integrability of the actual variance and allows subtraction under the integral. Joint reflection identifies the first term, so the displayed defect is exact even for noncentered signed f.

\[\operatorname{Var}_{S_y}(f)=\int f^2\,dS_y-(Tf(y))^2,\quad\int\operatorname{Var}_{S_y}(f)\,d\nu=\|f\|_{L^2(\nu)}^2-\|Tf\|_{L^2(\nu)}^2.\]
Corresponding Lean step

Poincare.variance; variance_eq_integral; variance_eq_sub; Integrable.congr; integral_sub; hvdef

6. Derive the true outer gradient domain

The pointwise parent proves actual differentiability of Tf. Mathlib measurable_fderiv followed by the continuous inverse Riesz map makes its true gradient strongly measurable. Its square is dominated by C_eta times the already integrable actual conditional variance, so it is integrable and the gradient lies in L2(nu). Fiber Poincare domains are not substituted for this outer domain.

\[\|\nabla Tf(y)\|^2\le C_\eta\operatorname{Var}_{S_y}(f),\quad C_\eta=\frac{(\eta^{-1}-\alpha)^2}{4(\alpha+\eta^{-1})},\quad\nabla Tf\in L^2(\nu).\]
Corresponding Lean step

measurable_fderiv; toDual.symm.continuous; Integrable.mono_nonneg; memLp_two_iff_integrable_sq_norm; hgradI; hgrad2

7. Integrate with the exact source coefficient

All domains have now been produced. Integrate the pointwise inequality, multiply by positive eta, and simplify the genuine positive denominators. Substitute the exact variance-defect identity. The coefficient remains sharp, including its zero at alphaeta=1; no arbitrary energy premise is introduced.

\[\eta C_\eta=\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)},\quad\eta\int\|\nabla Tf\|^2d\nu\le\eta C_\eta\int\operatorname{Var}_{S_y}(f)d\nu.\]
Corresponding Lean step

integral_mono; integral_const_mul; mul_le_mul_of_nonneg_left; hcoeff; hvdef

8. Consume the Gaussian precision and zero-dimensional boundaries

For the actual quadratic potential V=||x||²/2 with alpha=beta=eta=1, the coefficient is zero. The actual gradient energy therefore vanishes, while global differentiability, all three L2 domains, variance L1 and its defect identity remain available. A separate fully stated Test specializes these actual laws and domains to rank zero.

\[V=\tfrac12\|x\|^2,\quad\alpha=\beta=\eta=1\Longrightarrow\int\|\nabla Tf\|^2d\nu=0.\]
Corresponding Lean step

Tests.ProximalBPSConditionalGradientEnergy.gaussian_precision_outer_energy; rank_zero_actual_outer_energy

Lean verification

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

Lean proof · reflected_conditional_gradient_energy

Produce genuine laws and one common conditional kernel; Retain all actual finite second-moment domains; Integrate through the same disintegration; Use actual Gaussian reflection invariance; Produce the exact conditional variance defect; Derive the true outer gradient domain; Integrate with the exact source coefficient; Consume the Gaussian precision and zero-dimensional boundaries

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 reflected_conditional_gradient_energy
    {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
    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*η))) ∧
      ∀ (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) ν ∧
        (∫ y, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance
          (S y) f ∂ν) = (∫ y, (f y)^2 ∂ν) - (∫ y, (Tf y)^2 ∂ν) ∧
        η * (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤
          (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) *
            ((∫ y, (f y)^2 ∂ν) - (∫ y, (Tf y)^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
  obtain ⟨hZ,hJ,_⟩ := GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x a => (hH x a).1) hη
  have hexp : Integrable (fun x => Real.exp (-V x)) (volume : Measure E) := by
    by_contra hn
    exact (ne_of_gt hZ) (integral_undef hn)
  have hμ : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hexp
  letI := hμ
  letI : IsProbabilityMeasure J := hJ
  have hν : IsProbabilityMeasure ν := inferInstance
  letI := hν
  obtain ⟨R,S,hR,hS,hcond,hSR,hSd,hpoint⟩ :=
    ConditionalGradientVariance.reflected_conditional_gradient_variance hα hαβ hV hH hη hβη
  letI := hR
  letI := hS
  refine ⟨hμ,hJ,hν,R,S,hR,hS,hcond,hSR,hSd,?_⟩
  intro f hf hfc
  let Tf := fun y => ∫ u, f u ∂S y
  obtain ⟨M,hMb⟩ := hf.continuous.norm.bddAbove_range_of_hasCompactSupport hfc.norm
  have hM (u : E) : ‖f u‖ ≤ M := hMb (Set.mem_range_self u)
  have hM0 : 0 ≤ M := (norm_nonneg (f 0)).trans (hM 0)
  have hf2 : MemLp f 2 ν := MemLp.of_bound hf.continuous.aestronglyMeasurable M
    (Filter.Eventually.of_forall hM)
  have hfy2 (y : E) : MemLp f 2 (S y) :=
    MemLp.of_bound hf.continuous.aestronglyMeasurable M (Filter.Eventually.of_forall hM)
  have hTfsm : StronglyMeasurable Tf := hf.continuous.stronglyMeasurable.integral_kernel
  have hTfbound (y : E) : ‖Tf y‖ ≤ M := by
    simpa using norm_integral_le_of_norm_le_const (μ := S y) (Filter.Eventually.of_forall hM)
  have hTf2 : MemLp Tf 2 ν := MemLp.of_bound hTfsm.aestronglyMeasurable M
    (Filter.Eventually.of_forall hTfbound)
  let vf := fun y =>
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance (S y) f
  have hv (y : E) : vf y = (∫ u, (f u)^2 ∂S y)-(Tf y)^2 := by
    dsimp only [vf, AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance]
    rw [← variance_eq_integral (hfy2 y).aemeasurable, variance_eq_sub (hfy2 y)]
    rfl
  have hfsqsm : StronglyMeasurable (fun y => ∫ u, (f u)^2 ∂S y) :=
    (hf.continuous.pow 2).stronglyMeasurable.integral_kernel
  have hfsqbound (u : E) : ‖(f u)^2‖ ≤ M^2 := by
    rw [norm_pow]
    exact (sq_le_sq₀ (norm_nonneg _) hM0).mpr (hM u)
  have hfsq1 : MemLp (fun y => ∫ u, (f u)^2 ∂S y) 1 ν :=
    MemLp.of_bound hfsqsm.aestronglyMeasurable (M^2) (Filter.Eventually.of_forall
      fun y => by simpa using (norm_integral_le_of_norm_le_const (μ := S y)
        (Filter.Eventually.of_forall hfsqbound)))
  have hfsqI := hfsq1.integrable le_rfl
  have hvI : Integrable vf ν := (hfsqI.sub hTf2.integrable_sq).congr
    (Filter.Eventually.of_forall fun y => (hv y).symm)
  have hvdef : (∫ y, vf y ∂ν) = (∫ y, (f y)^2 ∂ν)-(∫ y, (Tf y)^2 ∂ν) := by
    rw [integral_congr_ae (Filter.Eventually.of_forall hv), integral_sub hfsqI hTf2.integrable_sq]
    rw [reflected_second_moment μ η hη R S f hf.continuous M hM hcond hSR]
  have hgradsm : StronglyMeasurable (gradient Tf) := by
    exact ((toDual ℝ E).symm.continuous.measurable.comp
      (measurable_fderiv (𝕜 := ℝ) (f := Tf))).stronglyMeasurable
  let C := (1/η-(α : ℝ))^2/(4*((α : ℝ)+1/η))
  have hgradI : Integrable (fun y => ‖gradient Tf y‖^2) ν :=
    (hvI.const_mul C).mono_nonneg (hgradsm.norm.pow 2).aestronglyMeasurable
      (Filter.Eventually.of_forall fun _ => sq_nonneg _)
      (Filter.Eventually.of_forall fun y => (hpoint f hf hfc y).2)
  have hgrad2 : MemLp (gradient Tf) 2 ν :=
    (memLp_two_iff_integrable_sq_norm hgradsm.aestronglyMeasurable).mpr hgradI
  refine ⟨fun y => (hpoint f hf hfc y).1,hf2,hTf2,hgrad2,hvI,hvdef,?_⟩
  have hi : (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤ C*(∫ y, vf y ∂ν) := by
    calc
      (∫ y, ‖gradient Tf y‖^2 ∂ν) ≤ ∫ y, C*vf y ∂ν :=
        integral_mono hgradI (hvI.const_mul C) (fun y => (hpoint f hf hfc y).2)
      _ = C*(∫ y, vf y ∂ν) := integral_const_mul _ _
  have hden : 0 < (α : ℝ)+1/η := by positivity
  have hnewden : 0 < 1+(α : ℝ)*η := by positivity
  have hcoeff : η*C = (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η)) := by
    dsimp only [C]
    field_simp [ne_of_gt hη,ne_of_gt hden,ne_of_gt hnewden]
    <;> ring
  calc
    η*(∫ y, ‖gradient Tf y‖^2 ∂ν) ≤ η*(C*(∫ y, vf y ∂ν)) :=
      mul_le_mul_of_nonneg_left hi hη.le
    _ = (η*C)*(∫ y, vf y ∂ν) := by ring
    _ = (1-(α : ℝ)*η)^2/(4*(1+(α : ℝ)*η))*
        ((∫ y, (f y)^2 ∂ν)-(∫ y, (Tf y)^2 ∂ν)) := by rw [hcoeff,hvdef]

end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientEnergy

Exact module and namespace context

Scope and omitted-condition boundaries
  • Smooth compact outer(C.2) exact coefficient and actual conditional variance-defect identity with all probability/measurability/L2/integrability domains internal. FiniteHilbert/rank0 authored extension. Full L2-to-H1/closed outer gradient/B.13 literal operator norm-square adapters/spectral C.3/halfturn/full mains/errors/cost/composition remain separate. Actual focused3888PASS; independent wholeproof/blind/source/exactcommit/shared admission pending.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasureTheory.isProbabilityMeasure_tilted
  • MeasureTheory.integral_undef
  • MeasureTheory.Measure.isProbabilityMeasure_map
  • MeasureTheory.Measure.IsCondKernel.disintegrate
  • MeasureTheory.Measure.fst_map_swap
  • MeasureTheory.Measure.integral_compProd
  • MeasureTheory.integral_map_of_stronglyMeasurable
  • MeasureTheory.StronglyMeasurable.integral_kernel
  • MeasureTheory.MemLp.of_bound
  • MeasureTheory.norm_integral_le_of_norm_le_const
  • MeasureTheory.MemLp.integrable_sq
  • ProbabilityTheory.variance_eq_integral
  • ProbabilityTheory.variance_eq_sub
  • measurable_fderiv
  • InnerProductSpace.toDual
  • MeasureTheory.Integrable.mono_nonneg
  • MeasureTheory.memLp_two_iff_integrable_sq_norm
  • MeasureTheory.integral_mono
  • MeasureTheory.integral_const_mul
  • MeasureTheory.integral_sub
  • MeasureTheory.integral_congr_ae

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.