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

GaussianReflectedMean: 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. C1 regularity of the literal reflected Gaussian posterior mean
Samplinglib mathematical lesson

C1 regularity of the literal reflected Gaussian posterior mean

AutoSamplingTheory.TechnicalLemmas.Measure.GaussianReflectedMean.gaussian_reflected_mean_c1 · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert space equipped with its Borel measurable structure, including rank zero. Let μ be any probability measure, η>0, and f:E→ℝ a globally C1 function with compact support. For every y∈E define R_y=μ.tilted(x↦−‖x−y‖²/(2η)) and S_y=(x↦2x−y)_#R_y. Then the exact function m(y)=∫f(u)S_y(du) is globally C1. These are the specified everywhere-defined posterior and reflection laws; no arbitrary AE conditional version is substituted. Moment, input density, domination, normalization, derivative-continuity and closed-gradient certificates are not premises. This is explicitly attributed authored analytic background for the paper’s normalized-density differentiation with its Gibbs input and smooth compact tests.

\[R_y(dx)=\frac{e^{-\|x-y\|^2/(2\eta)}}{Z(y)}\mu(dx),\quad S_y=(2x-y)_\#R_y,\quad m(y)=\frac{N(y)}{Z(y)}\in C^1,\quad N(y)=\int f(2x-y)e^{-\|y-x\|^2/(2\eta)}\mu(dx).\]
Lean statement · gaussian_reflected_mean_c1

Let E be a finite-dimensional real Hilbert space equipped with its Borel measurable structure, including rank zero. Let μ be any probability measure, η>0, and f:E→ℝ a globally C1 function with compact support. For every y∈E define R_y=μ.tilted(x↦−‖x−y‖²/(2η)) and S_y=(x↦2x−y)_#R_y. Then the exact function m(y)=∫f(u)S_y(du) is globally C1. These are the specified everywhere-defined posterior and reflection laws; no arbitrary AE conditional version is substituted. Moment, input density, domination, normalization, derivative-continuity and closed-gradient certificates are not premises. This is explicitly attributed authored analytic background for the paper’s normalized-density differentiation with its Gibbs input and smooth compact tests.

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 gaussian_reflected_mean_c1
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η)
    {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    let S := fun y : E => (R y).map (fun x : E => (2:ℝ) • x-y)
    ContDiff ℝ 1 (fun y : E => ∫ u, f u ∂S y)

Exact module and namespace context

Proof roadmap

  1. 1Bound the compact observer and its actual derivative

    C1 gives continuous f and continuous Frechet derivative. Compact support of f also gives compact support of its derivative. Compactness therefore supplies finite global bounds Mf and Md. Introduce the literal Gaussian weight K, weighted observer F and normalizing integral Z; the probability measure makes every constant bound integrable.

  2. 2Keep both genuine parameter derivatives and a uniform Gaussian bound

    The weight derivative is K′=−(K/η)〈y−x,·〉. The reflection parameter derivative is −Id, giving −Df(2x−y). The product rule retains both terms. The exponential estimate K‖y−x‖²≤2η and r≤1+r² give a uniform bound on K′; combine it with compact observer bounds. No input moment is used.

  3. 3Differentiate the actual weighted numerator under the integral

    Continuity in x gives precise AEStrong measurability for F and its actual Frechet derivative G. The observer bound proves genuine L1 of F. The uniform derivative bound is integrable under μ. Apply the pinned global dominated Frechet differentiation theorem on the whole parameter space, deriving the derivative of N from actual G.

  4. 4Prove continuous derivative, hence C1 numerator

    For every fixed x, G(y,x) is continuous in y because f and its derivative are continuous and the Gaussian/affine factors are continuous. The same global bound gives dominated continuity of the CLM-valued integral D(y). The genuine derivative identity and continuous D produce C1 N.

  5. 5Identify the literal every-y normalized mean before quotient calculus

    Reuse the existing Gaussian-convolution positive C2 normalizer. Positivity of its exact density prefactor times Z makes Z nonzero everywhere. Internally show Gaussian likelihood L1, so the actual tilt is a probability; bounded f then yields posterior L1 and mapped-observer L1 before using integral_map. The actual integral_tilted identity and norm symmetry identify exactly the same mean N/Z at every y. C1 numerator and positive C2 denominator conclude C1 of this literal mean.

  6. 6Consume the actual PBPS input and check a noncentered rank-zero mean

    The existing macroscopic-energy theorem produces probability of the source Gibbs μ under unchanged curvature and step bounds. The existing GaussianConditionalKernel constructs a true Markov conditional R for the same augmentation J and identifies its literal fiber at every y, so the new theorem applies to its reflected mean. This does not assert equality to the separate source-volume S density. The rank-zero standard Gaussian posterior/reflection yields the noncentered observer1 with real mean1 and actual Frechet derivative0.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real Hilbert/Borel space E; rank zero included as an explicit authored extension.
  • Any actual probability measure μ, any η>0 and any globally C1 real observer f with compact support; no centering or finite-moment/input-density premise.
  • R_y and S_y are exactly the displayed quadratic tilt and affine reflected pushforward at every y. The source-volume Gibbs density identity is a separate downstream adapter.
  • All observer/derivative bounds, measurability, genuine L1, dominated differentiation, continuous integrated derivative and positive normalization are internal outputs, not convenience binders.

Mathematical proof

1. Bound the compact observer and its actual derivative

C1 gives continuous f and continuous Frechet derivative. Compact support of f also gives compact support of its derivative. Compactness therefore supplies finite global bounds Mf and Md. Introduce the literal Gaussian weight K, weighted observer F and normalizing integral Z; the probability measure makes every constant bound integrable.

\[\|f(z)\|\le M_f,\quad\|Df(z)\|\le M_d,\quad K(y,x)=e^{-\|y-x\|^2/(2\eta)},\quad F(y,x)=K(y,x)f(2x-y).\]
Corresponding Lean step

hdfC; HasCompactSupport.exists_bound_of_continuous; HasCompactSupport.fderiv; K/F/N/D/Z

2. Keep both genuine parameter derivatives and a uniform Gaussian bound

The weight derivative is K′=−(K/η)〈y−x,·〉. The reflection parameter derivative is −Id, giving −Df(2x−y). The product rule retains both terms. The exponential estimate K‖y−x‖²≤2η and r≤1+r² give a uniform bound on K′; combine it with compact observer bounds. No input moment is used.

\[D_yF(y,x)[v]=-K(y,x)Df(2x-y)[v]-\frac{f(2x-y)K(y,x)}{\eta}\langle y-x,v\rangle,\quad 0<K\le1,\quad K\|y-x\|^2\le2\eta,\quad\|D_yF\|\le M_d+M_f\frac{1+2\eta}{\eta}.\]
Corresponding Lean step

hK; Real.mul_exp_neg_le_exp_neg_one; hKderiv; hKbound; hGbound; hFderiv; actual compiled chain-rule structure conversion

3. Differentiate the actual weighted numerator under the integral

Continuity in x gives precise AEStrong measurability for F and its actual Frechet derivative G. The observer bound proves genuine L1 of F. The uniform derivative bound is integrable under μ. Apply the pinned global dominated Frechet differentiation theorem on the whole parameter space, deriving the derivative of N from actual G.

\[N(y)=\int F(y,x)\mu(dx),\quad DN(y)=\int D_yF(y,x)\mu(dx),\quad F(y,\cdot)\in L^1(\mu),\quad\|D_yF\|\le M_d+M_f(1+2\eta)/\eta\in L^1(\mu).\]
Corresponding Lean step

hFmeas; hGmeas; hFI; hdN; hasFDerivAt_integral_of_dominated_of_fderiv_le (global namespace)

4. Prove continuous derivative, hence C1 numerator

For every fixed x, G(y,x) is continuous in y because f and its derivative are continuous and the Gaussian/affine factors are continuous. The same global bound gives dominated continuity of the CLM-valued integral D(y). The genuine derivative identity and continuous D produce C1 N.

\[D(y)=\int G(y,x)\mu(dx)\in C^0(E,E\to\mathbb R),\qquad DN=D,\qquad N\in C^1(E).\]
Corresponding Lean step

hDC; MeasureTheory.continuous_of_dominated; hNC; contDiff_one_iff_hasFDerivAt

5. Identify the literal every-y normalized mean before quotient calculus

Reuse the existing Gaussian-convolution positive C2 normalizer. Positivity of its exact density prefactor times Z makes Z nonzero everywhere. Internally show Gaussian likelihood L1, so the actual tilt is a probability; bounded f then yields posterior L1 and mapped-observer L1 before using integral_map. The actual integral_tilted identity and norm symmetry identify exactly the same mean N/Z at every y. C1 numerator and positive C2 denominator conclude C1 of this literal mean.

\[Z(y)=\int K(y,x)\mu(dx)>0,\quad Z\in C^2,\quad \int f\,dS_y=\int f(2x-y)\,dR_y=\frac{N(y)}{Z(y)},\quad m=N/Z\in C^1.\]
Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_potential_c2; hZC; hZ; hKI; hlike; isProbabilityMeasure_tilted; hobs; hmapI; integral_map; MeasureTheory.integral_tilted; hmean; ContDiff.div

6. Consume the actual PBPS input and check a noncentered rank-zero mean

The existing macroscopic-energy theorem produces probability of the source Gibbs μ under unchanged curvature and step bounds. The existing GaussianConditionalKernel constructs a true Markov conditional R for the same augmentation J and identifies its literal fiber at every y, so the new theorem applies to its reflected mean. This does not assert equality to the separate source-volume S density. The rank-zero standard Gaussian posterior/reflection yields the noncentered observer1 with real mean1 and actual Frechet derivative0.

\[\mu=dx.\operatorname{tilted}(-V),\quad J=\operatorname{law}(X,X+\sqrt\eta G),\quad R_y=\mu.\operatorname{tilted}(-\|x-y\|^2/(2\eta))\ \forall y;\qquad\dim E=0,\ f=1:\ m\equiv1,\ Dm\equiv0.\]
Corresponding Lean step

Tests.ProximalBPSGaussianReflectedMean.actual_pbps_reflected_kernel_mean; rank_zero_noncentered_mean; actual PBPS50 probability and GaussianConditionalKernel (Test only)

Lean verification

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

Lean proof · gaussian_reflected_mean_c1

Bound the compact observer and its actual derivative; Keep both genuine parameter derivatives and a uniform Gaussian bound; Differentiate the actual weighted numerator under the integral; Prove continuous derivative, hence C1 numerator; Identify the literal every-y normalized mean before quotient calculus; Consume the actual PBPS input and check a noncentered rank-zero mean

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 gaussian_reflected_mean_c1
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) [IsProbabilityMeasure μ] {η : ℝ} (hη : 0 < η)
    {f : E → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    let S := fun y : E => (R y).map (fun x : E => (2:ℝ) • x-y)
    ContDiff ℝ 1 (fun y : E => ∫ u, f u ∂S y)
 := by
  let K := fun y x : E => Real.exp (-‖y-x‖^2/(2*η))
  let K' := fun y x : E => (-K y x/η) • innerSL ℝ (y-x)
  let F := fun y x : E => K y x * f ((2:ℝ) • x-y)
  let G := fun y x : E => K y x • (-fderiv ℝ f ((2:ℝ) • x-y)) +
    f ((2:ℝ) • x-y) • K' y x
  let N := fun y : E => ∫ x, F y x ∂μ
  let D := fun y : E => ∫ x, G y x ∂μ
  let Z := fun y : E => ∫ x, K y x ∂μ
  have hdfC : Continuous (fderiv ℝ f) := hf.continuous_fderiv one_ne_zero
  obtain ⟨Mf, hMf⟩ := hc.exists_bound_of_continuous hf.continuous
  obtain ⟨Md, hMd⟩ := (hc.fderiv ℝ).exists_bound_of_continuous hdfC
  have hMf0 : 0 ≤ Mf := (norm_nonneg (f 0)).trans (hMf 0)
  have hK (y x : E) : 0 < K y x ∧ K y x ≤ 1 ∧ K y x * ‖y-x‖^2 ≤ 2*η := by
    have hp : 0 < K y x := Real.exp_pos _
    have h1 : K y x ≤ 1 := Real.exp_le_one_iff.mpr
      (div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) (by positivity))
    have hb := Real.mul_exp_neg_le_exp_neg_one (‖y-x‖^2/(2*η))
    have he : Real.exp (-1) ≤ 1 := Real.exp_le_one_iff.mpr (by norm_num)
    have hb' : K y x * (‖y-x‖^2/(2*η)) ≤ 1 := by
      simpa [K, mul_comm, neg_div] using hb.trans he
    have heq : K y x * (‖y-x‖^2/(2*η)) = (K y x * ‖y-x‖^2)/(2*η) := by ring
    rw [heq, div_le_iff₀ (by positivity)] at hb'
    exact ⟨hp,h1,by simpa using hb'⟩
  have hKderiv (y x : E) : HasFDerivAt (fun z => K z x) (K' y x) y := by
    have hd := (((hasFDerivAt_id y).sub_const x).norm_sq.const_mul (-1/(2*η))).exp
    convert hd using 1
    · funext z; dsimp only [K,id]; congr 1; ring
    · ext v
      have he : -‖y-x‖^2/(2*η) = (-1/(2*η))*‖y-x‖^2 := by ring
      simp only [K',K,he,smul_apply,ContinuousLinearMap.comp_apply,
        ContinuousLinearMap.id_apply,smul_eq_mul,innerSL_apply_apply,id]
      ring
  have hKbound (y x : E) : ‖K' y x‖ ≤ (1+2*η)/η := by
    obtain ⟨hp,h1,h2⟩ := hK y x
    have hr : ‖y-x‖ ≤ 1+‖y-x‖^2 := by nlinarith [sq_nonneg (‖y-x‖-1)]
    have hb : K y x * ‖y-x‖ ≤ 1+2*η := by
      calc
        _ ≤ K y x * (1+‖y-x‖^2) := mul_le_mul_of_nonneg_left hr hp.le
        _ ≤ 1+2*η := by nlinarith
    dsimp only [K']
    rw [norm_smul,Real.norm_eq_abs,abs_div,abs_neg,abs_of_pos hp,
      abs_of_pos hη,innerSL_apply_norm,div_mul_eq_mul_div,div_le_div_iff_of_pos_right hη]
    exact hb
  have hGbound (y x : E) : ‖G y x‖ ≤ Md + Mf*((1+2*η)/η) := by
    have hk := hK y x
    calc
      _ ≤ ‖K y x • (-fderiv ℝ f ((2:ℝ) • x-y))‖ +
          ‖f ((2:ℝ) • x-y) • K' y x‖ := norm_add_le _ _
      _ = K y x * ‖fderiv ℝ f ((2:ℝ) • x-y)‖ +
          ‖f ((2:ℝ) • x-y)‖ * ‖K' y x‖ := by
            rw [norm_smul,norm_smul,norm_neg,Real.norm_eq_abs,abs_of_pos hk.1]
      _ ≤ 1*Md + Mf*((1+2*η)/η) := add_le_add
        (mul_le_mul hk.2.1 (hMd _) (norm_nonneg _) (by norm_num))
        (mul_le_mul (hMf _) (hKbound y x) (norm_nonneg _) hMf0)
      _ = _ := by ring
  have hFmeas (y : E) : AEStronglyMeasurable (F y) μ := by
    apply Continuous.aestronglyMeasurable
    have hk : Continuous (K y) := by unfold K; fun_prop
    exact hk.mul (hf.continuous.comp (by fun_prop))
  have hGmeas (y : E) : AEStronglyMeasurable (G y) μ := by
    apply Continuous.aestronglyMeasurable
    dsimp only [G,K',K]
    have hd : Continuous (fun x : E => fderiv ℝ f ((2:ℝ) • x-y)) :=
      hdfC.comp (by fun_prop)
    have ho : Continuous (fun x : E => f ((2:ℝ) • x-y)) := hf.continuous.comp (by fun_prop)
    fun_prop
  have hFI (y : E) : Integrable (F y) μ := by
    apply (integrable_const Mf).mono' (hFmeas y)
    filter_upwards with x
    dsimp only [F]
    rw [norm_mul,Real.norm_eq_abs,abs_of_pos (hK y x).1]
    calc
      _ ≤ 1*Mf := mul_le_mul (hK y x).2.1 (hMf _) (norm_nonneg _) (by norm_num)
      _ = _ := one_mul _
  have hFderiv (y x : E) : HasFDerivAt (fun z => F z x) (G y x) y := by
    have ha := (hasFDerivAt_id (𝕜 := ℝ) y).const_sub ((2:ℝ) • x)
    have ho := (hf.differentiable_one ((2:ℝ) • x-y)).hasFDerivAt.comp y ha
    have ho' : HasFDerivAt (fun z : E => f ((2:ℝ) • x-z))
        (-fderiv ℝ f ((2:ℝ) • x-y)) y := by
      convert ho using 1 <;> first | rfl | (ext v; simp)
    exact (hKderiv y x).mul ho'
  have hdN (y : E) : HasFDerivAt N (D y) y := by
    apply hasFDerivAt_integral_of_dominated_of_fderiv_le (s := Set.univ)
      (bound := fun _ => Md+Mf*((1+2*η)/η)) Filter.univ_mem
    · exact Filter.Eventually.of_forall hFmeas
    · exact hFI y
    · exact hGmeas y
    · exact Filter.Eventually.of_forall (fun x z _ => hGbound z x)
    · exact integrable_const _
    · exact Filter.Eventually.of_forall (fun x z _ => hFderiv z x)
  have hDC : Continuous D := by
    apply continuous_of_dominated hGmeas
      (bound := fun _ => Md+Mf*((1+2*η)/η))
      (fun y => Filter.Eventually.of_forall (fun x => hGbound y x)) (integrable_const _)
    filter_upwards with x
    dsimp only [G,K',K]
    have hd : Continuous (fun y : E => fderiv ℝ f ((2:ℝ) • x-y)) := hdfC.comp (by fun_prop)
    have ho : Continuous (fun y : E => f ((2:ℝ) • x-y)) := hf.continuous.comp (by fun_prop)
    fun_prop
  have hNC : ContDiff ℝ 1 N := contDiff_one_iff_hasFDerivAt.mpr ⟨D,hDC,hdN⟩
  have hparent := GaussianConvolutionRegularity.gaussian_convolution_potential_c2 μ hη
  have hZC : ContDiff ℝ 2 Z := hparent.2.2.1
  have hZ (y : E) : Z y ≠ 0 := by
    have hp := hparent.2.1 y
    intro hz
    change 0 < ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E * Z y at hp
    rw [hz,mul_zero] at hp
    exact lt_irrefl _ hp
  have hKI (y : E) : Integrable (K y) μ := by
    apply (integrable_const (1:ℝ)).mono' (by unfold K; fun_prop)
    filter_upwards with x
    rw [Real.norm_eq_abs,abs_of_pos (hK y x).1]
    exact (hK y x).2.1
  have hmean (y : E) :
      (∫ u, f u ∂((μ.tilted (fun x => -‖x-y‖^2/(2*η))).map
        (fun x : E => (2:ℝ) • x-y))) = N y / Z y := by
    have hlike : Integrable (fun x : E => Real.exp (-‖x-y‖^2/(2*η))) μ := by
      simpa only [K,norm_sub_rev] using hKI y
    have : IsProbabilityMeasure (μ.tilted (fun x => -‖x-y‖^2/(2*η))) :=
      isProbabilityMeasure_tilted hlike
    have hobs : Integrable (fun x : E => f ((2:ℝ) • x-y))
        (μ.tilted (fun x => -‖x-y‖^2/(2*η))) := by
      apply (integrable_const Mf).mono' (hf.continuous.comp (by fun_prop)).aestronglyMeasurable
      exact Filter.Eventually.of_forall (fun x => hMf _)
    have hmapI : Integrable f ((μ.tilted (fun x => -‖x-y‖^2/(2*η))).map
        (fun x : E => (2:ℝ) • x-y)) :=
      (integrable_map_measure hf.continuous.aestronglyMeasurable (by fun_prop)).mpr hobs
    rw [integral_map (by fun_prop) hmapI.aestronglyMeasurable,integral_tilted]
    have hw (x : E) : Real.exp (-‖x-y‖^2/(2*η)) = K y x := by
      dsimp [K]; rw [norm_sub_rev x y]
    simp_rw [hw,smul_eq_mul]
    rw [← integral_div]
    apply integral_congr_ae
    filter_upwards with x
    dsimp [N,Z,F]
    ring
  change ContDiff ℝ 1 (fun y : E => ∫ u, f u ∂((μ.tilted
    (fun x => -‖x-y‖^2/(2*η))).map (fun x : E => (2:ℝ) • x-y)))
  simp_rw [hmean]
  exact hNC.div (hZC.of_le (by norm_num)) hZ

end
end AutoSamplingTheory.TechnicalLemmas.Measure.GaussianReflectedMean

Exact module and namespace context

Scope and omitted-condition boundaries
  • The literal reflected Gaussian posterior mean is globally C1 for any compact C1 real observer and any probability input/positive eta on finite real Hilbert/Borel E, including rank zero. Actual source-volume S_y pointwise identity, actual Tf closed-gradient membership, rough B.13/Gamma/main/errors/nonexplosion/cost/composition remain separate. Focused3893 passed; independent mathematics/source/exact-commit/shared integration remain pending.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • HasCompactSupport.exists_bound_of_continuous
  • HasCompactSupport.fderiv
  • ContDiff.continuous_fderiv
  • Real.mul_exp_neg_le_exp_neg_one
  • HasFDerivAt.comp
  • HasFDerivAt.mul
  • hasFDerivAt_integral_of_dominated_of_fderiv_le
  • MeasureTheory.continuous_of_dominated
  • contDiff_one_iff_hasFDerivAt
  • MeasureTheory.isProbabilityMeasure_tilted
  • MeasureTheory.integrable_map_measure
  • MeasureTheory.integral_map
  • MeasureTheory.integral_tilted
  • ContDiff.div

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.