AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential

No declaration docstring.

theorem integrable_and_integrable_exp_centered_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E]
    {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) :
    MeasureTheory.Integrable f μ ∧ ∀ t : ℝ,
      MeasureTheory.Integrable
        (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ := by
  have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by
    have hd := hf.dist_le_mul x 0
    simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd
    calc
      |f x| = |(f x-f 0)+f 0| := by congr 1; ring
      _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _
      _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl
  have hi : Integrable f μ :=
    (((IsGaussian.integrable_id (μ := μ)).norm.const_mul (L : ℝ)).add
      (integrable_const |f 0|)).mono' hf.continuous.aestronglyMeasurable
        (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs, Pi.add_apply, id_eq] using hbound x)
  refine ⟨hi,fun t => ?_⟩
  obtain ⟨C,hC,hint⟩ := IsGaussian.exists_integrable_exp_sq μ
  let b : ℝ := |t| *(L : ℝ)
  let D : ℝ := |t| *(|f 0|+|∫ z, f z ∂μ|)
  have hb : 0 ≤ b := mul_nonneg (abs_nonneg _) L.coe_nonneg
  have hdom (x : E) : t*(f x-∫ z, f z ∂μ) ≤
      D+C⁻¹*b^2+C*‖x‖^2 := by
    have hlin : t*(f x-∫ z, f z ∂μ) ≤ b*‖x‖+D := by
      calc
        _ ≤ |t*(f x-∫ z, f z ∂μ)| := le_abs_self _
        _ = |t| *|f x-∫ z, f z ∂μ| := abs_mul _ _
        _ ≤ |t| *(|f x|+|∫ z, f z ∂μ|) :=
          mul_le_mul_of_nonneg_left (by simpa only [sub_zero, zero_sub, abs_neg] using
            (abs_sub_le (f x) 0 (∫ z, f z ∂μ))) (abs_nonneg _)
        _ ≤ |t| *((L : ℝ)*‖x‖+|f 0|+|∫ z, f z ∂μ|) :=
          mul_le_mul_of_nonneg_left (add_le_add (hbound x) le_rfl) (abs_nonneg _)
        _ = b*‖x‖+D := by dsimp [b,D]; ring
    have hy : 2*‖x‖*b ≤ C*‖x‖^2+C⁻¹*b^2 := two_mul_le_add_mul_sq hC
    have hnon : 0 ≤ b*‖x‖ := mul_nonneg hb (norm_nonneg _)
    nlinarith
  apply (hint.const_mul (Real.exp (D+C⁻¹*b^2))).mono'
    (by fun_prop)
  filter_upwards with x
  rw [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _),← Real.exp_add]
  exact Real.exp_le_exp.mpr (hdom x)
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:33published source at ed709a7f320dOpen detailed card

Excerpt truncated; the exact source link is authoritative.

# Gaussian exponential domains and sharp standard Gaussian concentration Fernique domination gives first moments and every signed centered exponential moment on a real second-countable Banach Borel space. For the actual standard Gaussian on a finite-dimensional real Hilbert space, rotation and conditional Stein yield the sharp coefficient 1/2; normalized smooth convolution removes the internal C1 restriction without changing the Lipschitz constant. SPHMC's actual Gaussian output consumes these results with its own Bochner mean. Degenerate dimensions, zero constants and all signed parameters are included. -/ noncomputable section open MeasureTheory ProbabilityTheory open scoped NNReal ENNReal Convolution Topology namespace AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential theorem integrable_and_integrable_exp_centered_of_lipschitz {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) : MeasureTheory.Integrable f μ ∧ ∀ t : ℝ, MeasureTheory.Integrable (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ := by have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by have hd := hf.dist_le_mul x 0 simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd calc |f x| = |(f x-f 0)+f 0| := by congr 1; ring _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _ _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl have hi : Integrable f μ := (((IsGaussian.integrable_id (μ := μ)).norm.const_mul (L : ℝ)).add (integrable_const |f 0|)).mono' hf.continuous.aestronglyMeasurable (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs, Pi.add_apply, id_eq] using hbound x) refine ⟨hi,fun t => ?_⟩ obtain ⟨C,hC,hint⟩ := IsGaussian.exists_integrable_exp_sq μ let b : ℝ := |t| *(L : ℝ) let D : ℝ := |t| *(|f 0|+|∫ z, f z ∂μ|) have hb : 0 ≤ b := mul_nonneg (abs_nonneg _) L.coe_nonneg have hdom (x : E) : t*(f x-∫ z, f z ∂μ) ≤ D+C⁻¹*b^2+C*‖x‖^2 := by have hlin : t*(f x-∫ z, f z ∂μ) ≤ b*‖x‖+D := by calc _ ≤ |t*(f x-∫ z, f z ∂μ)| := le_abs_self _ _ = |t| *|f x-∫ z, f z ∂μ| := abs_mul _ _ _ ≤ |t| *(|f x|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (by simpa only [sub_zero, zero_sub, abs_neg] using (abs_sub_le (f x) 0 (∫ z, f z ∂μ))) (abs_nonneg _) _ ≤ |t| *((L : ℝ)*‖x‖+|f 0|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (add_le_add (hbound x) le_rfl) (abs_nonneg _) _ = b*‖x‖+D := by dsimp [b,D]; ring have hy : 2*‖x‖*b ≤ C*‖x‖^2+C⁻¹*b^2 := two_mul_le_add_mul_sq hC have hnon : 0 ≤ b*‖x‖ := mul_nonneg hb (norm_nonneg _) nlinarith apply (hint.const_mul (Real.exp (D+C⁻¹*b^2))).mono' (by fun_prop) filter_upwards with x rw [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _),← Real.exp_add] exact Real.exp_le_exp.mpr (hdom x) /- The zero-Lipschitz branch of the sealed sharp target is internal; this is not an assertion of the remaining positive-dimensional concentration bound.

private theorem centered_exp_integral_of_lipschitz_zero
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {f : E → ℝ} (hf : LipschitzWith 0 f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E))
      ∂stdGaussian E) = 1 := by
  have hconst : f = fun _ => f 0 := by
    funext x
    have hd := hf.dist_le_mul x 0
    simp only [NNReal.coe_zero, zero_mul] at hd
    exact dist_eq_zero.mp (le_antisymm hd (dist_nonneg))
  rw [hconst]
  simp

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:80published source at ed709a7f320d

No declaration docstring.

private theorem centered_exp_integral_of_subsingleton
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    [Subsingleton E] (f : E → ℝ) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E))
      ∂stdGaussian E) = 1 := by
  have hconst : f = fun _ => f 0 := by
    funext x
    exact congrArg f (Subsingleton.elim x 0)
  rw [hconst]
  simp

/- Radial domination is used on the actual product Gaussian when differentiating
the rotation integral. Its constants are domination constants, not the sharp
concentration coefficient. -/

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:94published source at ed709a7f320d

# Gaussian exponential domains and sharp standard Gaussian concentration Fernique domination gives first moments and every signed centered exponential moment on a real second-countable Banach Borel space. For the actual standard Gaussian on a finite-dimensional real Hilbert space, rotation and conditional Stein yield the sharp coefficient 1/2; normalized smooth convolution removes the internal C1 restriction without changing the Lipschitz constant. SPHMC's actual Gaussian output consumes these results with its own Bochner mean. Degenerate dimensions, zero constants and all signed parameters are included. -/ noncomputable section open MeasureTheory ProbabilityTheory open scoped NNReal ENNReal Convolution Topology namespace AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential theorem integrable_and_integrable_exp_centered_of_lipschitz {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) : MeasureTheory.Integrable f μ ∧ ∀ t : ℝ, MeasureTheory.Integrable (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ := by have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by have hd := hf.dist_le_mul x 0 simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd calc |f x| = |(f x-f 0)+f 0| := by congr 1; ring _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _ _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl have hi : Integrable f μ := (((IsGaussian.integrable_id (μ := μ)).norm.const_mul (L : ℝ)).add (integrable_const |f 0|)).mono' hf.continuous.aestronglyMeasurable (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs, Pi.add_apply, id_eq] using hbound x) refine ⟨hi,fun t => ?_⟩ obtain ⟨C,hC,hint⟩ := IsGaussian.exists_integrable_exp_sq μ let b : ℝ := |t| *(L : ℝ) let D : ℝ := |t| *(|f 0|+|∫ z, f z ∂μ|) have hb : 0 ≤ b := mul_nonneg (abs_nonneg _) L.coe_nonneg have hdom (x : E) : t*(f x-∫ z, f z ∂μ) ≤ D+C⁻¹*b^2+C*‖x‖^2 := by have hlin : t*(f x-∫ z, f z ∂μ) ≤ b*‖x‖+D := by calc _ ≤ |t*(f x-∫ z, f z ∂μ)| := le_abs_self _ _ = |t| *|f x-∫ z, f z ∂μ| := abs_mul _ _ _ ≤ |t| *(|f x|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (by simpa only [sub_zero, zero_sub, abs_neg] using (abs_sub_le (f x) 0 (∫ z, f z ∂μ))) (abs_nonneg _) _ ≤ |t| *((L : ℝ)*‖x‖+|f 0|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (add_le_add (hbound x) le_rfl) (abs_nonneg _) _ = b*‖x‖+D := by dsimp [b,D]; ring have hy : 2*‖x‖*b ≤ C*‖x‖^2+C⁻¹*b^2 := two_mul_le_add_mul_sq hC have hnon : 0 ≤ b*‖x‖ := mul_nonneg hb (norm_nonneg _) nlinarith apply (hint.const_mul (Real.exp (D+C⁻¹*b^2))).mono' (by fun_prop) filter_upwards with x rw [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _),← Real.exp_add] exact Real.exp_le_exp.mpr (hdom x) /- The zero-Lipschitz branch of the sealed sharp target is internal; this is not an assertion of the remaining positive-dimensional concentration bound. -/ private theorem centered_exp_integral_of_lipschitz_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℝ} (hf : LipschitzWith 0 f) (t : ℝ) : (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) = 1 := by have hconst : f = fun _ => f 0 := by funext x have hd := hf.dist_le_mul x 0 simp only [NNReal.coe_zero, zero_mul] at hd exact dist_eq_zero.mp (le_antisymm hd (dist_nonneg)) rw [hconst] simp private theorem centered_exp_integral_of_subsingleton {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Subsingleton E] (f : E → ℝ) (t : ℝ) : (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) = 1 := by have hconst : f = fun _ => f 0 := by funext x exact congrArg f (Subsingleton.elim x 0) rw [hconst] simp /- Radial domination is used on the actual product Gaussian when differentiating the rotation integral. Its constants are domination constants, not the sharp concentration coefficient.

private theorem gaussian_radial_exponential_integrable
    {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H]
    [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
    {μ : Measure H} [IsGaussian μ] (a : ℝ) :
    Integrable (fun x : H => Real.exp (a * ‖x‖)) μ := by
  have hi := (integrable_and_integrable_exp_centered_of_lipschitz
    (μ := μ) (lipschitzWith_one_norm : LipschitzWith 1 (norm : H → ℝ))).2 a
  apply (hi.const_mul (Real.exp (a * ∫ x : H, ‖x‖ ∂μ))).congr
  filter_upwards with x
  rw [← Real.exp_add]
  congr 1
  ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:109published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_polynomial_radial_integrable
    {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H]
    [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
    {μ : Measure H} [IsGaussian μ] (a : ℝ) :
    Integrable (fun x : H => (1 + ‖x‖)^2 * Real.exp (a * ‖x‖)) μ := by
  apply (gaussian_radial_exponential_integrable (μ := μ) (a + 2)).mono' (by fun_prop)
  filter_upwards with x
  rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]
  have hs : (1 + ‖x‖)^2 ≤ (Real.exp ‖x‖)^2 :=
    (sq_le_sq₀ (by positivity) (Real.exp_pos _).le).2
      (by simpa only [add_comm] using Real.add_one_le_exp ‖x‖)
  calc
    _ ≤ (Real.exp ‖x‖)^2 * Real.exp (a * ‖x‖) :=
      mul_le_mul_of_nonneg_right hs (Real.exp_pos _).le
    _ = _ := by
      rw [pow_two, ← Real.exp_add, ← Real.exp_add]
      congr 1
      ring

section GaussianDensity
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:122published source at ed709a7f320d

No declaration docstring.

private def standardWeight (x : E) : ℝ :=
  ((Real.sqrt (2 * Real.pi))⁻¹) ^ Module.finrank ℝ E * Real.exp (-‖x‖^2 / 2)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:145published source at ed709a7f320d

No declaration docstring.

private theorem standardWeight_pos (x : E) : 0 < standardWeight x := by
  dsimp [standardWeight]
  positivity

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:148published source at ed709a7f320d

No declaration docstring.

private theorem standardGaussian_density :
    stdGaussian E = (volume : Measure E).withDensity
      (fun x => ENNReal.ofReal (standardWeight x)) := by
  have h := AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity
    (E := E) 1 (by norm_num)
  simpa only [Real.sqrt_one, one_smul, Measure.map_id', mul_one,
    standardWeight] using h

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:152published source at ed709a7f320d

No declaration docstring.

private theorem standardGaussian_weighted_integral (g : E → ℝ) :
    (∫ x, g x ∂stdGaussian E) = ∫ x, standardWeight x * g x := by
  rw [standardGaussian_density]
  rw [integral_withDensity_eq_integral_toReal_smul (by unfold standardWeight; fun_prop)
    (ae_of_all _ fun _ => ENNReal.ofReal_lt_top) g]
  apply integral_congr_ae
  filter_upwards with x
  simp only [ENNReal.toReal_ofReal (standardWeight_pos x).le, smul_eq_mul]

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:160published source at ed709a7f320d

No declaration docstring.

private theorem standardGaussian_weighted_integrable {g : E → ℝ}
    (hg : Integrable g (stdGaussian E)) :
    Integrable (fun x => standardWeight x * g x) (volume : Measure E) := by
  rw [standardGaussian_density] at hg
  have h := (integrable_withDensity_iff (by unfold standardWeight; fun_prop)
    (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)).1 hg
  simpa only [ENNReal.toReal_ofReal (standardWeight_pos _).le, mul_comm] using h

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:169published source at ed709a7f320d

No declaration docstring.

private theorem standardWeight_hasFDerivAt (x : E) :
    HasFDerivAt (standardWeight : E → ℝ)
      (-(standardWeight x) • innerSL ℝ x) x := by
  let c : ℝ := ((Real.sqrt (2 * Real.pi))⁻¹) ^ Module.finrank ℝ E
  have h := (((hasFDerivAt_id x).norm_sq.const_mul (-1 / 2 : ℝ)).exp).const_mul c
  convert h using 1
  all_goals try rfl
  · funext y
    dsimp only [standardWeight, c, id]
    congr 1
    ring
  · ext v
    dsimp only [standardWeight, c, id]
    simp only [smul_apply, smul_eq_mul, innerSL_apply_apply,
      ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply]
    have he : (-1 / 2 : ℝ) * ‖x‖^2 = -‖x‖^2 / 2 := by ring
    rw [he]
    ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:177published source at ed709a7f320d

No declaration docstring.

private theorem standardGaussian_stein_lipschitz_c1
    {f : E → ℝ} {L : ℝ≥0} (hf : ContDiff ℝ 1 f)
    (hLip : LipschitzWith L f) (v : E) :
    (∫ x, inner ℝ x v * f x ∂stdGaussian E) =
      ∫ x, fderiv ℝ f x v ∂stdGaussian E := by
  have hfi := (integrable_and_integrable_exp_centered_of_lipschitz
    (μ := stdGaussian E) hLip).1
  have hn : Integrable (fun x : E => ‖x‖) (stdGaussian E) := IsGaussian.integrable_id.norm
  have hsq := (StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian (E := E)).1
  have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by
    have hd := hLip.dist_le_mul x 0
    simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd
    calc
      |f x| = |(f x-f 0)+f 0| := by congr 1; ring
      _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _
      _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl
  have hixf : Integrable (fun x => inner ℝ x v*f x) (stdGaussian E) := by
    apply (((hsq.const_mul (L : ℝ)).add (hn.const_mul |f 0|)).const_mul ‖v‖).mono'
      (by fun_prop)
    filter_upwards with x
    change ‖inner ℝ x v*f x‖ ≤ ‖v‖*((L : ℝ)*‖x‖^2+|f 0| * ‖x‖)
    rw [norm_mul, Real.norm_eq_abs (f x)]
    calc
      ‖inner ℝ x v‖*|f x| ≤ (‖x‖*‖v‖)*((L : ℝ)*‖x‖+|f 0|) :=
        mul_le_mul (norm_inner_le_norm x v) (hbound x) (abs_nonneg _) (by positivity)
      _ = _ := by ring
  have hdf : Integrable (fun x => fderiv ℝ f x v) (stdGaussian E) := by
    apply (integrable_const ((L : ℝ)*‖v‖)).mono'
      ((hf.continuous_fderiv (by norm_num)).clm_apply continuous_const).aestronglyMeasurable
    filter_upwards with x
    exact (ContinuousLinearMap.le_opNorm _ _).trans
      (mul_le_mul_of_nonneg_right (norm_fderiv_le_of_lipschitz ℝ hLip) (norm_nonneg _))
  have hDw (x : E) : fderiv ℝ (standardWeight : E → ℝ) x v =
      -standardWeight x*inner ℝ x v := by
    rw [(standardWeight_hasFDerivAt x).fderiv]
    simp only [smul_apply, smul_eq_mul, innerSL_apply_apply]
  have hwp := standardGaussian_weighted_integrable hfi
  have hwdf := standardGaussian_weighted_integrable hdf
  have hwxf := standardGaussian_weighted_integrable hixf
  have hDwf : Integrable (fun x => fderiv ℝ (standardWeight : E → ℝ) x v*f x)
      (volume : Measure E) := by
    convert hwxf.neg using 1
    ext x
    rw [hDw]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:196published source at ed709a7f320d

Excerpt truncated; the exact source link is authoritative.

# Gaussian exponential domains and sharp standard Gaussian concentration Fernique domination gives first moments and every signed centered exponential moment on a real second-countable Banach Borel space. For the actual standard Gaussian on a finite-dimensional real Hilbert space, rotation and conditional Stein yield the sharp coefficient 1/2; normalized smooth convolution removes the internal C1 restriction without changing the Lipschitz constant. SPHMC's actual Gaussian output consumes these results with its own Bochner mean. Degenerate dimensions, zero constants and all signed parameters are included. -/ noncomputable section open MeasureTheory ProbabilityTheory open scoped NNReal ENNReal Convolution Topology namespace AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential theorem integrable_and_integrable_exp_centered_of_lipschitz {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) : MeasureTheory.Integrable f μ ∧ ∀ t : ℝ, MeasureTheory.Integrable (fun x => Real.exp (t * (f x - ∫ z, f z ∂μ))) μ := by have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by have hd := hf.dist_le_mul x 0 simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd calc |f x| = |(f x-f 0)+f 0| := by congr 1; ring _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _ _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl have hi : Integrable f μ := (((IsGaussian.integrable_id (μ := μ)).norm.const_mul (L : ℝ)).add (integrable_const |f 0|)).mono' hf.continuous.aestronglyMeasurable (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs, Pi.add_apply, id_eq] using hbound x) refine ⟨hi,fun t => ?_⟩ obtain ⟨C,hC,hint⟩ := IsGaussian.exists_integrable_exp_sq μ let b : ℝ := |t| *(L : ℝ) let D : ℝ := |t| *(|f 0|+|∫ z, f z ∂μ|) have hb : 0 ≤ b := mul_nonneg (abs_nonneg _) L.coe_nonneg have hdom (x : E) : t*(f x-∫ z, f z ∂μ) ≤ D+C⁻¹*b^2+C*‖x‖^2 := by have hlin : t*(f x-∫ z, f z ∂μ) ≤ b*‖x‖+D := by calc _ ≤ |t*(f x-∫ z, f z ∂μ)| := le_abs_self _ _ = |t| *|f x-∫ z, f z ∂μ| := abs_mul _ _ _ ≤ |t| *(|f x|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (by simpa only [sub_zero, zero_sub, abs_neg] using (abs_sub_le (f x) 0 (∫ z, f z ∂μ))) (abs_nonneg _) _ ≤ |t| *((L : ℝ)*‖x‖+|f 0|+|∫ z, f z ∂μ|) := mul_le_mul_of_nonneg_left (add_le_add (hbound x) le_rfl) (abs_nonneg _) _ = b*‖x‖+D := by dsimp [b,D]; ring have hy : 2*‖x‖*b ≤ C*‖x‖^2+C⁻¹*b^2 := two_mul_le_add_mul_sq hC have hnon : 0 ≤ b*‖x‖ := mul_nonneg hb (norm_nonneg _) nlinarith apply (hint.const_mul (Real.exp (D+C⁻¹*b^2))).mono' (by fun_prop) filter_upwards with x rw [Real.norm_eq_abs,abs_of_pos (Real.exp_pos _),← Real.exp_add] exact Real.exp_le_exp.mpr (hdom x) /- The zero-Lipschitz branch of the sealed sharp target is internal; this is not an assertion of the remaining positive-dimensional concentration bound. -/ private theorem centered_exp_integral_of_lipschitz_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℝ} (hf : LipschitzWith 0 f) (t : ℝ) : (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) = 1 := by have hconst : f = fun _ => f 0 := by funext x have hd := hf.dist_le_mul x 0 simp only [NNReal.coe_zero, zero_mul] at hd exact dist_eq_zero.mp (le_antisymm hd (dist_nonneg)) rw [hconst] simp private theorem centered_exp_integral_of_subsingleton {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Subsingleton E] (f : E → ℝ) (t : ℝ) : (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) = 1 := by have hconst : f = fun _ => f 0 := by funext x exact congrArg f (Subsingleton.elim x 0) rw [hconst] simp /- Radial domination is used on the actual product Gaussian when differentiating the rotation integral. Its constants are domination constants, not the sharp concentration coefficient. -/ private theorem gaussian_radial_exponential_integrable {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {μ : Measure H} [IsGaussian μ] (a : ℝ) : Integrable (fun x : H => Real.exp (a * ‖x‖)) μ := by have hi := (integrable_and_integrable_exp_centered_of_lipschitz (μ := μ) (lipschitzWith_one_norm : LipschitzWith 1 (norm : H → ℝ))).2 a apply (hi.const_mul (Real.exp (a * ∫ x : H, ‖x‖ ∂μ))).congr filter_upwards with x rw [← Real.exp_add] congr 1 ring private theorem gaussian_polynomial_radial_integrable {H : Type*} [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] {μ : Measure H} [IsGaussian μ] (a : ℝ) : Integrable (fun x : H => (1 + ‖x‖)^2 * Real.exp (a * ‖x‖)) μ := by apply (gaussian_radial_exponential_integrable (μ := μ) (a + 2)).mono' (by fun_prop) filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] have hs : (1 + ‖x‖)^2 ≤ (Real.exp ‖x‖)^2 := (sq_le_sq₀ (by positivity) (Real.exp_pos _).le).2 (by simpa only [add_comm] using Real.add_one_le_exp ‖x‖) calc _ ≤ (Real.exp ‖x‖)^2 * Real.exp (a * ‖x‖) := mul_le_mul_of_nonneg_right hs (Real.exp_pos _).le _ = _ := by rw [pow_two, ← Real.exp_add, ← Real.exp_add] congr 1 ring section GaussianDensity variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] private def standardWeight (x : E) : ℝ := ((Real.sqrt (2 * Real.pi))⁻¹) ^ Module.finrank ℝ E * Real.exp (-‖x‖^2 / 2) private theorem standardWeight_pos (x : E) : 0 < standardWeight x := by dsimp [standardWeight] positivity private theorem standardGaussian_density : stdGaussian E = (volume : Measure E).withDensity (fun x => ENNReal.ofReal (standardWeight x)) := by have h := AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity (E := E) 1 (by norm_num) simpa only [Real.sqrt_one, one_smul, Measure.map_id', mul_one, standardWeight] using h private theorem standardGaussian_weighted_integral (g : E → ℝ) : (∫ x, g x ∂stdGaussian E) = ∫ x, standardWeight x * g x := by rw [standardGaussian_density] rw [integral_withDensity_eq_integral_toReal_smul (by unfold standardWeight; fun_prop) (ae_of_all _ fun _ => ENNReal.ofReal_lt_top) g] apply integral_congr_ae filter_upwards with x simp only [ENNReal.toReal_ofReal (standardWeight_pos x).le, smul_eq_mul] private theorem standardGaussian_weighted_integrable {g : E → ℝ} (hg : Integrable g (stdGaussian E)) : Integrable (fun x => standardWeight x * g x) (volume : Measure E) := by rw [standardGaussian_density] at hg have h := (integrable_withDensity_iff (by unfold standardWeight; fun_prop) (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)).1 hg simpa only [ENNReal.toReal_ofReal (standardWeight_pos _).le, mul_comm] using h private theorem standardWeight_hasFDerivAt (x : E) : HasFDerivAt (standardWeight : E → ℝ) (-(standardWeight x) • innerSL ℝ x) x := by let c : ℝ := ((Real.sqrt (2 * Real.pi))⁻¹) ^ Module.finrank ℝ E have h := (((hasFDerivAt_id x).norm_sq.const_mul (-1 / 2 : ℝ)).exp).const_mul c convert h using 1 all_goals try rfl · funext y dsimp only [standardWeight, c, id] congr 1 ring · ext v dsimp only [standardWeight, c, id] simp only [smul_apply, smul_eq_mul, innerSL_apply_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] have he : (-1 / 2 : ℝ) * ‖x‖^2 = -‖x‖^2 / 2 := by ring rw [he] ring private theorem standardGaussian_stein_lipschitz_c1 {f : E → ℝ} {L : ℝ≥0} (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (v : E) : (∫ x, inner ℝ x v * f x ∂stdGaussian E) = ∫ x, fderiv ℝ f x v ∂stdGaussian E := by have hfi := (integrable_and_integrable_exp_centered_of_lipschitz (μ := stdGaussian E) hLip).1 have hn : Integrable (fun x : E => ‖x‖) (stdGaussian E) := IsGaussian.integrable_id.norm have hsq := (StdGaussianMoment.integrable_norm_sq_and_integral_stdGaussian (E := E)).1 have hbound (x : E) : |f x| ≤ (L : ℝ)*‖x‖+|f 0| := by have hd := hLip.dist_le_mul x 0 simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd calc |f x| = |(f x-f 0)+f 0| := by congr 1; ring _ ≤ |f x-f 0|+|f 0| := abs_add_le _ _ _ ≤ (L : ℝ)*‖x‖+|f 0| := add_le_add hd le_rfl have hixf : Integrable (fun x => inner ℝ x v*f x) (stdGaussian E) := by apply (((hsq.const_mul (L : ℝ)).add (hn.const_mul |f 0|)).const_mul ‖v‖).mono' (by fun_prop) filter_upwards with x change ‖inner ℝ x v*f x‖ ≤ ‖v‖*((L : ℝ)*‖x‖^2+|f 0| * ‖x‖) rw [norm_mul, Real.norm_eq_abs (f x)] calc ‖inner ℝ x v‖*|f x| ≤ (‖x‖*‖v‖)*((L : ℝ)*‖x‖+|f 0|) := mul_le_mul (norm_inner_le_norm x v) (hbound x) (abs_nonneg _) (by positivity) _ = _ := by ring have hdf : Integrable (fun x => fderiv ℝ f x v) (stdGaussian E) := by apply (integrable_const ((L : ℝ)*‖v‖)).mono' ((hf.continuous_fderiv (by norm_num)).clm_apply continuous_const).aestronglyMeasurable filter_upwards with x exact (ContinuousLinearMap.le_opNorm _ _).trans (mul_le_mul_of_nonneg_right (norm_fderiv_le_of_lipschitz ℝ hLip) (norm_nonneg _)) have hDw (x : E) : fderiv ℝ (standardWeight : E → ℝ) x v = -standardWeight x*inner ℝ x v := by rw [(standardWeight_hasFDerivAt x).fderiv] simp only [smul_apply, smul_eq_mul, innerSL_apply_apply] have hwp := standardGaussian_weighted_integrable hfi have hwdf := standardGaussian_weighted_integrable hdf have hwxf := standardGaussian_weighted_integrable hixf have hDwf : Integrable (fun x => fderiv ℝ (standardWeight : E → ℝ) x v*f x) (volume : Measure E) := by convert hwxf.neg using 1 ext x rw [hDw] simp only [Pi.neg_apply] ring have hparts := integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable hDwf hwdf hwp (fun x _ => (standardWeight_hasFDerivAt x).differentiableAt) (fun x _ => hf.differentiable_one x) rw [standardGaussian_weighted_integral, standardGaussian_weighted_integral] calc (∫ x, standardWeight x*(inner ℝ x v*f x)) = -(∫ x, fderiv ℝ (standardWeight : E → ℝ) x v*f x) := by rw [← integral_neg] apply integral_congr_ae filter_upwards with x rw [hDw] ring _ = ∫ x, standardWeight x*fderiv ℝ f x v := hparts.symm /- This uses Stein only for the affine pullback of the Lipschitz observable. The exponential test function is not asserted to be globally Lipschitz.

private theorem standardGaussian_stein_affine
    {f : E → ℝ} {L : ℝ≥0} (hf : ContDiff ℝ 1 f)
    (hLip : LipschitzWith L f) (c s : ℝ) (u a : E) :
    (∫ v, inner ℝ v a * f (c • u - s • v) ∂stdGaussian E) =
      -s * ∫ v, fderiv ℝ f (c • u - s • v) a ∂stdGaussian E := by
  have hca : ContDiff ℝ 1 (fun v : E => c • u - s • v) := by fun_prop
  have hla : LipschitzWith (L * Real.nnabs s) (fun v : E => f (c • u - s • v)) := by
    apply LipschitzWith.of_dist_le_mul
    intro x y
    calc
      _ ≤ (L : ℝ) * dist (c • u - s • x) (c • u - s • y) := hLip.dist_le_mul _ _
      _ = ((L * Real.nnabs s : ℝ≥0) : ℝ) * dist x y := by
        simp only [dist_eq_norm]
        rw [show (c • u - s • x) - (c • u - s • y) = s • (y - x) by module]
        rw [norm_smul, Real.norm_eq_abs, norm_sub_rev]
        simp only [NNReal.coe_mul, Real.coe_nnabs]
        ring
  have hd (v : E) :
      fderiv ℝ (fun v : E => f (c • u - s • v)) v a =
        -s * fderiv ℝ f (c • u - s • v) a := by
    have ha := ((hasFDerivAt_id (𝕜 := ℝ) v).const_smul s).const_sub (c • u)
    have hh := ((hf.differentiable_one _).hasFDerivAt.comp v ha).fderiv
    simp only [Function.comp_def, Pi.smul_apply, id_eq] at hh
    rw [hh]
    simp
  rw [standardGaussian_stein_lipschitz_c1
    (f := fun v => f (c • u - s • v)) (hf.comp hca) hla a]
  simp_rw [hd]
  exact integral_const_mul _ _

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:258published source at ed709a7f320d

No declaration docstring.

private theorem standardGaussian_rotation_integral
    (θ : ℝ) {h : E × E → ℝ} (hh : Continuous h) :
    (∫ p, h (ContinuousLinearMap.rotation θ p)
      ∂(stdGaussian E).prod (stdGaussian E)) =
      ∫ p, h p ∂(stdGaussian E).prod (stdGaussian E) := by
  have hm := IsGaussian.map_rotation_eq_self
    (μ := stdGaussian E) (integral_id_stdGaussian (E := E)) θ
  have hi := integral_map (μ := (stdGaussian E).prod (stdGaussian E))
    (ContinuousLinearMap.rotation θ).continuous.measurable.aemeasurable
    hh.aestronglyMeasurable
  rw [hm] at hi
  exact hi.symm

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:288published source at ed709a7f320d

No declaration docstring.

private def rotX (θ : ℝ) (p : E × E) : E :=
  Real.cos θ • p.1 + Real.sin θ • p.2

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:301published source at ed709a7f320d

No declaration docstring.

private def rotY (θ : ℝ) (p : E × E) : E :=
  -Real.sin θ • p.1 + Real.cos θ • p.2

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:304published source at ed709a7f320d

No declaration docstring.

private theorem norm_linear_pair_le_two {c s : ℝ}
    (hc : |c| ≤ 1) (hs : |s| ≤ 1) (p : E × E) :
    ‖c • p.1 + s • p.2‖ ≤ 2 * ‖p‖ := by
  calc
    _ ≤ ‖c • p.1‖ + ‖s • p.2‖ := norm_add_le _ _
    _ = |c| * ‖p.1‖ + |s| * ‖p.2‖ := by simp only [norm_smul, Real.norm_eq_abs]
    _ ≤ ‖p.1‖ + ‖p.2‖ := add_le_add
      (by simpa only [one_mul] using mul_le_mul_of_nonneg_right hc (norm_nonneg p.1))
      (by simpa only [one_mul] using mul_le_mul_of_nonneg_right hs (norm_nonneg p.2))
    _ ≤ 2 * ‖p‖ := by linarith [norm_fst_le p, norm_snd_le p]

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:307published source at ed709a7f320d

No declaration docstring.

private theorem norm_rotX_le (θ : ℝ) (p : E × E) : ‖rotX θ p‖ ≤ 2 * ‖p‖ :=
  norm_linear_pair_le_two (Real.abs_cos_le_one θ) (Real.abs_sin_le_one θ) p

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:318published source at ed709a7f320d

No declaration docstring.

private theorem norm_rotY_le (θ : ℝ) (p : E × E) : ‖rotY θ p‖ ≤ 2 * ‖p‖ :=
  norm_linear_pair_le_two (by simpa only [abs_neg] using Real.abs_sin_le_one θ)
    (Real.abs_cos_le_one θ) p

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:321published source at ed709a7f320d

No declaration docstring.

private theorem rotX_hasDerivAt (θ : ℝ) (p : E × E) :
    HasDerivAt (fun θ => rotX θ p) (rotY θ p) θ := by
  exact ((Real.hasDerivAt_cos θ).smul_const p.1).add
    ((Real.hasDerivAt_sin θ).smul_const p.2)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:325published source at ed709a7f320d

No declaration docstring.

private theorem lipschitz_growth_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (x : E) : |f x| ≤ (L : ℝ) * ‖x‖ + |f 0| := by
  have hd := hf.dist_le_mul x 0
  simp only [dist_eq_norm, sub_zero, Real.norm_eq_abs] at hd
  calc
    |f x| = |(f x - f 0) + f 0| := by congr 1; ring
    _ ≤ |f x - f 0| + |f 0| := abs_add_le _ _
    _ ≤ (L : ℝ) * ‖x‖ + |f 0| := add_le_add hd le_rfl

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:330published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t m θ : ℝ) (p : E × E) :
    Real.exp (t * (f (rotX θ p) - m)) ≤
      Real.exp (|t| * (|f 0| + |m|)) * Real.exp ((2 * |t| * (L : ℝ)) * ‖p‖) := by
  rw [← Real.exp_add]
  apply Real.exp_le_exp.mpr
  have hfrot : |f (rotX θ p)| ≤ (L : ℝ) * (2 * ‖p‖) + |f 0| :=
    (lipschitz_growth_bound hf _).trans
      (add_le_add (mul_le_mul_of_nonneg_left (norm_rotX_le θ p) L.coe_nonneg) le_rfl)
  calc
    _ ≤ |t * (f (rotX θ p) - m)| := le_abs_self _
    _ = |t| * |f (rotX θ p) - m| := abs_mul _ _
    _ ≤ |t| * (|f (rotX θ p)| + |m|) :=
      mul_le_mul_of_nonneg_left (abs_sub _ _) (abs_nonneg _)
    _ ≤ |t| * ((L : ℝ) * (2 * ‖p‖) + |f 0| + |m|) :=
      mul_le_mul_of_nonneg_left (add_le_add hfrot le_rfl) (abs_nonneg _)
    _ = _ := by ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:339published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_value_integrable {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t m θ : ℝ) :
    Integrable (fun p : E × E => f p.1 * Real.exp (t * (f (rotX θ p) - m)))
      ((stdGaussian E).prod (stdGaussian E)) := by
  let C : ℝ := (L : ℝ) + |f 0|
  let B : ℝ := Real.exp (|t| * (|f 0| + |m|))
  let A : ℝ := 2 * |t| * (L : ℝ)
  have hcont := hf.continuous
  apply ((gaussian_polynomial_radial_integrable
    (μ := (stdGaussian E).prod (stdGaussian E)) A).const_mul (C * B)).mono'
    (by unfold rotX; fun_prop)
  filter_upwards with p
  change ‖f p.1 * Real.exp (t * (f (rotX θ p) - m))‖ ≤
    (C * B) * ((1 + ‖p‖)^2 * Real.exp (A * ‖p‖))
  have hc : 0 ≤ C := by dsimp [C]; positivity
  have hg : |f p.1| ≤ C * (1 + ‖p‖) := by
    have h := (lipschitz_growth_bound hf p.1).trans
      (add_le_add (mul_le_mul_of_nonneg_left (norm_fst_le p) L.coe_nonneg) le_rfl)
    dsimp [C]
    nlinarith [norm_nonneg p, abs_nonneg (f 0)]
  have hp : 1 + ‖p‖ ≤ (1 + ‖p‖)^2 := by nlinarith [norm_nonneg p]
  rw [norm_mul, Real.norm_eq_abs (f p.1), Real.norm_eq_abs,
    abs_of_pos (Real.exp_pos _)]
  calc
    _ ≤ (C * (1 + ‖p‖)) * (B * Real.exp (A * ‖p‖)) :=
      mul_le_mul hg (rotated_laplace_bound hf t m θ p) (Real.exp_pos _).le
        (mul_nonneg hc (by positivity))
    _ = (C * B * Real.exp (A * ‖p‖)) * (1 + ‖p‖) := by ring
    _ ≤ (C * B * Real.exp (A * ‖p‖)) * (1 + ‖p‖)^2 :=
      mul_le_mul_of_nonneg_left hp (by dsimp [B]; positivity)
    _ = _ := by ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:357published source at ed709a7f320d

No declaration docstring.

private def rotatedLaplaceDerivative (f : E → ℝ) (t m θ : ℝ) (p : E × E) : ℝ :=
  f p.1 * (Real.exp (t * (f (rotX θ p) - m)) * (t * fderiv ℝ f (rotX θ p) (rotY θ p)))

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:389published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_hasDerivAt {f : E → ℝ}
    (hf : ContDiff ℝ 1 f) (t m θ : ℝ) (p : E × E) :
    HasDerivAt (fun θ => f p.1 * Real.exp (t * (f (rotX θ p) - m)))
      (rotatedLaplaceDerivative f t m θ p) θ := by
  have hd := (hf.differentiable_one (rotX θ p)).hasFDerivAt.comp_hasDerivAt θ
    (rotX_hasDerivAt θ p)
  simpa only [Function.comp_def, rotatedLaplaceDerivative] using
    (((hd.sub_const m).const_mul t).exp.const_mul (f p.1))

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:392published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_derivative_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t m θ : ℝ) (p : E × E) :
    ‖rotatedLaplaceDerivative f t m θ p‖ ≤
      (2 * ((L : ℝ) + |f 0|) * Real.exp (|t| * (|f 0| + |m|)) * |t| * (L : ℝ)) *
        ((1 + ‖p‖)^2 * Real.exp ((2 * |t| * (L : ℝ)) * ‖p‖)) := by
  let C : ℝ := (L : ℝ) + |f 0|
  let B : ℝ := Real.exp (|t| * (|f 0| + |m|))
  let A : ℝ := 2 * |t| * (L : ℝ)
  have hc : 0 ≤ C := by dsimp [C]; positivity
  have hb : 0 < B := Real.exp_pos _
  have hg : |f p.1| ≤ C * (1 + ‖p‖) := by
    have h := (lipschitz_growth_bound hf p.1).trans
      (add_le_add (mul_le_mul_of_nonneg_left (norm_fst_le p) L.coe_nonneg) le_rfl)
    dsimp [C]
    nlinarith [norm_nonneg p, abs_nonneg (f 0)]
  have hd : |fderiv ℝ f (rotX θ p) (rotY θ p)| ≤ (L : ℝ) * (2 * ‖p‖) := by
    rw [← Real.norm_eq_abs]
    exact ((ContinuousLinearMap.le_opNorm _ _).trans
      (mul_le_mul_of_nonneg_right (norm_fderiv_le_of_lipschitz ℝ hf) (norm_nonneg _))).trans
        (mul_le_mul_of_nonneg_left (norm_rotY_le θ p) L.coe_nonneg)
  change ‖f p.1 * (Real.exp (t * (f (rotX θ p) - m)) *
    (t * fderiv ℝ f (rotX θ p) (rotY θ p)))‖ ≤
      (2 * C * B * |t| * (L : ℝ)) * ((1 + ‖p‖)^2 * Real.exp (A * ‖p‖))
  rw [Real.norm_eq_abs]
  simp only [abs_mul, abs_of_pos (Real.exp_pos _)]
  calc
    _ ≤ (C * (1 + ‖p‖)) * ((B * Real.exp (A * ‖p‖)) *
        (|t| * ((L : ℝ) * (2 * ‖p‖)))) := by
      gcongr
      exact rotated_laplace_bound hf t m θ p
    _ = (2 * C * B * |t| * (L : ℝ) * Real.exp (A * ‖p‖)) * ((1 + ‖p‖) * ‖p‖) := by ring
    _ ≤ (2 * C * B * |t| * (L : ℝ) * Real.exp (A * ‖p‖)) * (1 + ‖p‖)^2 :=
      mul_le_mul_of_nonneg_left (by nlinarith [norm_nonneg p]) (by positivity)
    _ = _ := by ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:401published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_derivative_integrable {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m θ : ℝ) :
    Integrable (rotatedLaplaceDerivative f t m θ) ((stdGaussian E).prod (stdGaussian E)) := by
  have hcf := hf.continuous
  have hdf := hf.continuous_fderiv (by norm_num)
  apply ((gaussian_polynomial_radial_integrable
    (μ := (stdGaussian E).prod (stdGaussian E)) (2 * |t| * (L : ℝ))).const_mul
      (2 * ((L : ℝ) + |f 0|) * Real.exp (|t| * (|f 0| + |m|)) * |t| * (L : ℝ))).mono'
    (by unfold rotatedLaplaceDerivative rotX rotY; fun_prop)
  exact ae_of_all _ (rotated_laplace_derivative_bound hLip t m θ)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:436published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_integral_hasDerivAt {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m θ : ℝ) :
    HasDerivAt
      (fun θ => ∫ p : E × E, f p.1 * Real.exp (t * (f (rotX θ p) - m))
        ∂(stdGaussian E).prod (stdGaussian E))
      (∫ p, rotatedLaplaceDerivative f t m θ p
        ∂(stdGaussian E).prod (stdGaussian E)) θ := by
  have hcf := hf.continuous
  have hdf := hf.continuous_fderiv (by norm_num)
  have h := hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (μ := (stdGaussian E).prod (stdGaussian E))
    (F := fun θ p => f p.1 * Real.exp (t * (f (rotX θ p) - m)))
    (F' := fun θ => rotatedLaplaceDerivative f t m θ)
    (s := Set.univ)
    (bound := fun p =>
      (2 * ((L : ℝ) + |f 0|) * Real.exp (|t| * (|f 0| + |m|)) * |t| * (L : ℝ)) *
        ((1 + ‖p‖)^2 * Real.exp ((2 * |t| * (L : ℝ)) * ‖p‖)))
    (by simp)
    (Filter.Eventually.of_forall fun _ => by unfold rotX; fun_prop)
    (rotated_laplace_value_integrable hLip t m θ)
    (by unfold rotatedLaplaceDerivative rotX rotY; fun_prop)
    (ae_of_all _ fun p θ _ => rotated_laplace_derivative_bound hLip t m θ p)
    ((gaussian_polynomial_radial_integrable
      (μ := (stdGaussian E).prod (stdGaussian E)) (2 * |t| * (L : ℝ))).const_mul _)
    (ae_of_all _ fun p θ _ => rotated_laplace_hasDerivAt hf t m θ p)
  exact h.2

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:447published source at ed709a7f320d

No declaration docstring.

private theorem affine_stein_laplace_slice {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m c s : ℝ) (u : E) :
    (∫ v, f (c • u - s • v) *
      (Real.exp (t * (f u - m)) * (t * fderiv ℝ f u v)) ∂stdGaussian E) =
      -s * Real.exp (t * (f u - m)) * t *
        ∫ v, fderiv ℝ f (c • u - s • v)
          ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)) ∂stdGaussian E := by
  let a : E := (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)
  have ha (v : E) : inner ℝ v a = fderiv ℝ f u v := by
    rw [real_inner_comm]
    exact InnerProductSpace.toDual_symm_apply
  have he : (fun v => f (c • u - s • v) *
      (Real.exp (t * (f u - m)) * (t * fderiv ℝ f u v))) =
      fun v => (Real.exp (t * (f u - m)) * t) * (inner ℝ v a * f (c • u - s • v)) := by
    funext v
    rw [ha]
    ring
  rw [he, integral_const_mul, standardGaussian_stein_affine hf hLip c s u a]
  ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:474published source at ed709a7f320d

No declaration docstring.

private theorem affine_directional_derivative_integral_norm_le {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (c s : ℝ) (u : E) :
    ‖∫ v, fderiv ℝ f (c • u - s • v)
      ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)) ∂stdGaussian E‖ ≤ (L : ℝ)^2 := by
  let a : E := (InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)
  have hn : ‖a‖ ≤ (L : ℝ) := by
    dsimp [a]
    rw [LinearIsometryEquiv.norm_map]
    exact norm_fderiv_le_of_lipschitz ℝ hLip
  have hb (v : E) : ‖fderiv ℝ f (c • u - s • v) a‖ ≤ (L : ℝ)^2 := by
    calc
      _ ≤ ‖fderiv ℝ f (c • u - s • v)‖ * ‖a‖ := ContinuousLinearMap.le_opNorm _ _
      _ ≤ (L : ℝ) * (L : ℝ) :=
        mul_le_mul (norm_fderiv_le_of_lipschitz ℝ hLip) hn (norm_nonneg _) L.coe_nonneg
      _ = _ := by ring
  have h := norm_integral_le_of_norm_le_const (μ := stdGaussian E) (ae_of_all _ hb)
  simpa [a] using h

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:494published source at ed709a7f320d

No declaration docstring.

private theorem rotation_inverse_first (θ : ℝ) (p : E × E) :
    Real.cos θ • rotX θ p - Real.sin θ • rotY θ p = p.1 := by
  have hc : Real.cos θ * Real.cos θ + Real.sin θ * Real.sin θ = 1 := by
    nlinarith [Real.sin_sq_add_cos_sq θ]
  calc
    _ = (Real.cos θ * Real.cos θ + Real.sin θ * Real.sin θ) • p.1 +
        (Real.cos θ * Real.sin θ - Real.sin θ * Real.cos θ) • p.2 := by
      dsimp [rotX, rotY]
      module
    _ = _ := by simp [hc, mul_comm]

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:512published source at ed709a7f320d

No declaration docstring.

private theorem rotated_laplace_derivative_integral_identity {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m θ : ℝ) :
    (∫ p, rotatedLaplaceDerivative f t m θ p
      ∂(stdGaussian E).prod (stdGaussian E)) =
      (-Real.sin θ * t) * ∫ u, Real.exp (t * (f u - m)) *
        (∫ v, fderiv ℝ f (Real.cos θ • u - Real.sin θ • v)
          ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)) ∂stdGaussian E)
        ∂stdGaussian E := by
  let h : E × E → ℝ := fun p => f (Real.cos θ • p.1 - Real.sin θ • p.2) *
    (Real.exp (t * (f p.1 - m)) * (t * fderiv ℝ f p.1 p.2))
  have hcf := hf.continuous
  have hdf := hf.continuous_fderiv (by norm_num)
  have hcont : Continuous h := by dsimp [h]; fun_prop
  have he (p : E × E) : h (ContinuousLinearMap.rotation θ p) =
      rotatedLaplaceDerivative f t m θ p := by
    change f (Real.cos θ • rotX θ p - Real.sin θ • rotY θ p) *
      (Real.exp (t * (f (rotX θ p) - m)) * (t * fderiv ℝ f (rotX θ p) (rotY θ p))) = _
    rw [rotation_inverse_first]
    rfl
  have hm := IsGaussian.map_rotation_eq_self
    (μ := stdGaussian E) (integral_id_stdGaussian (E := E)) θ
  have hi : Integrable h ((stdGaussian E).prod (stdGaussian E)) := by
    have hic : Integrable (h ∘ ContinuousLinearMap.rotation θ)
        ((stdGaussian E).prod (stdGaussian E)) :=
      (rotated_laplace_derivative_integrable hf hLip t m θ).congr
        (ae_of_all _ fun p => (he p).symm)
    have hmap := (integrable_map_measure
      (μ := (stdGaussian E).prod (stdGaussian E)) hcont.aestronglyMeasurable
      (ContinuousLinearMap.rotation θ).continuous.measurable.aemeasurable).2 hic
    rwa [hm] at hmap
  calc
    _ = ∫ p, h (ContinuousLinearMap.rotation θ p)
        ∂(stdGaussian E).prod (stdGaussian E) := integral_congr_ae
          (ae_of_all _ fun p => (he p).symm)
    _ = ∫ p, h p ∂(stdGaussian E).prod (stdGaussian E) :=
      standardGaussian_rotation_integral θ hcont
    _ = ∫ u, ∫ v, h (u, v) ∂stdGaussian E ∂stdGaussian E := integral_prod _ hi
    _ = ∫ u, -Real.sin θ * Real.exp (t * (f u - m)) * t *
        (∫ v, fderiv ℝ f (Real.cos θ • u - Real.sin θ • v)
          ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)) ∂stdGaussian E)
        ∂stdGaussian E := by
      apply integral_congr_ae
      filter_upwards with u
      exact affine_stein_laplace_slice hf hLip t m (Real.cos θ) (Real.sin θ) u
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:523published source at ed709a7f320d

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

private theorem rotated_laplace_derivative_integral_lower_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m θ : ℝ)
    (ht : 0 ≤ t) (hs : 0 ≤ Real.sin θ) :
    (-Real.sin θ * t) * ((L : ℝ)^2 * ∫ u, Real.exp (t * (f u - m)) ∂stdGaussian E) ≤
      ∫ p, rotatedLaplaceDerivative f t m θ p
        ∂(stdGaussian E).prod (stdGaussian E) := by
  let I : E → ℝ := fun u => ∫ v, fderiv ℝ f (Real.cos θ • u - Real.sin θ • v)
    ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f u)) ∂stdGaussian E
  have hdf := hf.continuous_fderiv (by norm_num)
  have hcf := hf.continuous
  have hI : StronglyMeasurable I := by
    have hcont : Continuous (fun p : E × E =>
        fderiv ℝ f (Real.cos θ • p.1 - Real.sin θ • p.2)
          ((InnerProductSpace.toDual ℝ E).symm (fderiv ℝ f p.1))) := by fun_prop
    exact hcont.stronglyMeasurable.integral_prod_right'
  have hIn (u : E) : ‖I u‖ ≤ (L : ℝ)^2 :=
    affine_directional_derivative_integral_norm_le hf hLip (Real.cos θ) (Real.sin θ) u
  have hExp : Integrable (fun u => Real.exp (t * (f u - m))) (stdGaussian E) := by
    have he := (integrable_and_integrable_exp_centered_of_lipschitz
      (μ := stdGaussian E) hLip).2 t
    apply (he.const_mul (Real.exp (t * (∫ u, f u ∂stdGaussian E - m)))).congr
    filter_upwards with u
    rw [← Real.exp_add]
    congr 1
    ring
  have hJ : Integrable (fun u => Real.exp (t * (f u - m)) * I u) (stdGaussian E) := by
    apply (hExp.mul_const ((L : ℝ)^2)).mono'
      ((by fun_prop : Continuous (fun u => Real.exp (t * (f u - m)))).aestronglyMeasurable.mul
        hI.aestronglyMeasurable)
    filter_upwards with u
    change ‖Real.exp (t * (f u - m)) * I u‖ ≤ Real.exp (t * (f u - m)) * (L : ℝ)^2
    simp only [norm_mul, Real.norm_eq_abs (Real.exp _), abs_of_pos (Real.exp_pos _)]
    exact mul_le_mul_of_nonneg_left (hIn u) (Real.exp_pos _).le
  have hupper : (∫ u, Real.exp (t * (f u - m)) * I u ∂stdGaussian E) ≤
      (L : ℝ)^2 * ∫ u, Real.exp (t * (f u - m)) ∂stdGaussian E := by
    rw [← integral_const_mul]
    apply integral_mono hJ (hExp.const_mul _)
    intro u
    change Real.exp (t * (f u - m)) * I u ≤ (L : ℝ)^2 * Real.exp (t * (f u - m))
    rw [mul_comm ((L : ℝ)^2)]
    exact mul_le_mul_of_nonneg_left
      ((le_abs_self (I u)).trans (by simpa only [Real.norm_eq_abs] using hIn u))
      (Real.exp_pos _).le
  rw [rotated_laplace_derivative_integral_identity hf hLip]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:573published source at ed709a7f320d

Excerpt truncated; the exact source link is authoritative.

No declaration docstring.

private theorem gaussian_laplace_covariance_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t m : ℝ) (ht : 0 ≤ t) :
    (∫ x, f x * Real.exp (t * (f x - m)) ∂stdGaussian E) -
      (∫ x, f x ∂stdGaussian E) * (∫ x, Real.exp (t * (f x - m)) ∂stdGaussian E) ≤
        t * (L : ℝ)^2 * ∫ x, Real.exp (t * (f x - m)) ∂stdGaussian E := by
  let F : ℝ → ℝ := fun θ => ∫ p : E × E, f p.1 * Real.exp (t * (f (rotX θ p) - m))
    ∂(stdGaussian E).prod (stdGaussian E)
  let M : ℝ := ∫ x, Real.exp (t * (f x - m)) ∂stdGaussian E
  let C : ℝ := t * (L : ℝ)^2 * M
  let H : ℝ → ℝ := fun θ => F θ - Real.cos θ * C
  let D : ℝ → ℝ := fun θ => ∫ p, rotatedLaplaceDerivative f t m θ p
    ∂(stdGaussian E).prod (stdGaussian E)
  have hd (θ : ℝ) : HasDerivAt H (D θ + Real.sin θ * C) θ := by
    simpa only [H, F, D, Pi.sub_apply, neg_mul, sub_neg_eq_add] using!
      (rotated_laplace_integral_hasDerivAt hf hLip t m θ).sub
        ((Real.hasDerivAt_cos θ).mul_const C)
  have hcont : Continuous H := continuous_iff_continuousAt.2 (fun θ => (hd θ).continuousAt)
  have hm : MonotoneOn H (Set.Icc 0 (Real.pi / 2)) := by
    apply monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _) hcont.continuousOn
      (fun θ _ => (hd θ).hasDerivWithinAt)
    intro θ hθ
    have hθ' := interior_subset hθ
    have hs : 0 ≤ Real.sin θ := Real.sin_nonneg_of_nonneg_of_le_pi hθ'.1
      (by linarith [hθ'.2, Real.pi_pos])
    have hb := rotated_laplace_derivative_integral_lower_bound hf hLip t m θ ht hs
    change 0 ≤ D θ + Real.sin θ * C
    dsimp [D, C, M]
    nlinarith
  have hzero : F 0 = ∫ x, f x * Real.exp (t * (f x - m)) ∂stdGaussian E := by
    dsimp [F]
    rw [integral_prod _ (rotated_laplace_value_integrable hLip t m 0)]
    simp [rotX]
  have hpi : F (Real.pi / 2) = (∫ x, f x ∂stdGaussian E) * M := by
    dsimp [F, M]
    rw [integral_prod _ (rotated_laplace_value_integrable hLip t m (Real.pi / 2))]
    simp only [rotX, Real.cos_pi_div_two, Real.sin_pi_div_two, zero_smul, one_smul,
      zero_add, integral_const_mul, integral_mul_const]
  have hh := hm (show 0 ∈ Set.Icc 0 (Real.pi / 2) by constructor; rfl; positivity)
    (show Real.pi / 2 ∈ Set.Icc 0 (Real.pi / 2) by constructor; positivity; rfl)
    (by positivity)
  simp only [H, Real.cos_zero, one_mul, Real.cos_pi_div_two, zero_mul, sub_zero,
    hzero, hpi] at hh
  dsimp [C, M] at hh
  linarith

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:619published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_centered_integrableExpSet {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) :
    integrableExpSet (fun x => f x - ∫ z, f z ∂stdGaussian E) (stdGaussian E) = Set.univ := by
  apply Set.eq_univ_of_forall
  intro t
  exact (integrable_and_integrable_exp_centered_of_lipschitz (μ := stdGaussian E) hf).2 t

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:664published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_centered_laplace_hasDerivAt {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t : ℝ) :
    HasDerivAt
      (fun t => ∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E)
      (∫ x, (f x - ∫ z, f z ∂stdGaussian E) *
        Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) t := by
  have ht : t ∈ interior (integrableExpSet
      (fun x => f x - ∫ z, f z ∂stdGaussian E) (stdGaussian E)) := by
    rw [gaussian_centered_integrableExpSet hf, interior_univ]
    exact Set.mem_univ t
  convert! hasDerivAt_mgf ht using 1

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:671published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_centered_laplace_derivative_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t : ℝ) (ht : 0 ≤ t) :
    (∫ x, (f x - ∫ z, f z ∂stdGaussian E) *
      Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) ≤
      t * (L : ℝ)^2 * ∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E := by
  let m : ℝ := ∫ z, f z ∂stdGaussian E
  have he := (integrable_and_integrable_exp_centered_of_lipschitz (μ := stdGaussian E) hLip).2 t
  have hti : t ∈ interior (integrableExpSet (fun x => f x - m) (stdGaussian E)) := by
    rw [gaussian_centered_integrableExpSet hLip, interior_univ]
    exact Set.mem_univ t
  have hp : Integrable (fun x => (f x - m) * Real.exp (t * (f x - m))) (stdGaussian E) := by
    simpa only [pow_one] using integrable_pow_mul_exp_of_mem_interior_integrableExpSet hti 1
  have hfp : Integrable (fun x => f x * Real.exp (t * (f x - m))) (stdGaussian E) := by
    apply (hp.add (he.const_mul m)).congr
    filter_upwards with x
    change (f x - m) * Real.exp (t * (f x - m)) + m * Real.exp (t * (f x - m)) = _
    ring
  change (∫ x, (f x - m) * Real.exp (t * (f x - m)) ∂stdGaussian E) ≤ _
  calc
    _ = (∫ x, f x * Real.exp (t * (f x - m)) ∂stdGaussian E) -
        m * (∫ x, Real.exp (t * (f x - m)) ∂stdGaussian E) := by
      rw [← integral_const_mul, ← integral_sub hfp (he.const_mul m)]
      apply integral_congr_ae
      filter_upwards with x
      ring
    _ ≤ _ := gaussian_laplace_covariance_bound hf hLip t m ht

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:683published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_centered_laplace_bound_c1_nonneg {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t : ℝ) (ht : 0 ≤ t) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) ≤
      Real.exp ((L : ℝ)^2 * t^2 / 2) := by
  let M : ℝ → ℝ := fun s => ∫ x, Real.exp (s * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E
  let D : ℝ → ℝ := fun s => ∫ x, (f x - ∫ z, f z ∂stdGaussian E) *
    Real.exp (s * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E
  let W : ℝ → ℝ := fun s => Real.exp ((-(L : ℝ)^2 / 2) * s^2) * M s
  have hd (s : ℝ) : HasDerivAt W
      (Real.exp ((-(L : ℝ)^2 / 2) * s^2) * (D s - (L : ℝ)^2 * s * M s)) s := by
    have hq : HasDerivAt (fun y : ℝ => (-(L : ℝ)^2 / 2) * y^2) (-(L : ℝ)^2 * s) s := by
      convert! ((hasDerivAt_id s).pow 2).const_mul (-(L : ℝ)^2 / 2) using 1 <;>
        simp only [id_eq] <;> ring
    convert! hq.exp.mul (gaussian_centered_laplace_hasDerivAt hLip s) using 1 <;>
      dsimp only [W, M, D] <;> ring
  have hcont : Continuous W := continuous_iff_continuousAt.2 (fun s => (hd s).continuousAt)
  have hm : AntitoneOn W (Set.Ici 0) := by
    apply antitoneOn_of_hasDerivWithinAt_nonpos (convex_Ici _) hcont.continuousOn
      (fun s _ => (hd s).hasDerivWithinAt)
    intro s hs
    have hs' : 0 ≤ s := interior_subset hs
    have hb := gaussian_centered_laplace_derivative_bound hf hLip s hs'
    apply mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le
    dsimp [D, M]
    nlinarith
  have hw := hm (show 0 ∈ Set.Ici (0 : ℝ) by simp)
    (show t ∈ Set.Ici (0 : ℝ) by simpa only [Set.mem_Ici] using ht) ht
  have hw' : Real.exp ((-(L : ℝ)^2 / 2) * t^2) * M t ≤ 1 := by
    simpa [W, M] using hw
  change M t ≤ _
  calc
    M t = Real.exp ((L : ℝ)^2 * t^2 / 2) *
        (Real.exp ((-(L : ℝ)^2 / 2) * t^2) * M t) := by
      rw [← mul_assoc, ← Real.exp_add]
      have hz : (L : ℝ)^2 * t^2 / 2 + (-(L : ℝ)^2 / 2) * t^2 = 0 := by ring
      rw [hz, Real.exp_zero, one_mul]
    _ ≤ Real.exp ((L : ℝ)^2 * t^2 / 2) * 1 :=
      mul_le_mul_of_nonneg_left hw' (Real.exp_pos _).le
    _ = _ := mul_one _

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:710published source at ed709a7f320d

No declaration docstring.

private theorem gaussian_centered_laplace_bound_c1 {f : E → ℝ} {L : ℝ≥0}
    (hf : ContDiff ℝ 1 f) (hLip : LipschitzWith L f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E) ≤
      Real.exp ((L : ℝ)^2 * t^2 / 2) := by
  by_cases ht : 0 ≤ t
  · exact gaussian_centered_laplace_bound_c1_nonneg hf hLip t ht
  · have h := gaussian_centered_laplace_bound_c1_nonneg hf.neg hLip.neg (-t) (by linarith)
    simp only [Pi.neg_apply, integral_neg] at h
    convert! h using 1
    · apply integral_congr_ae
      filter_upwards with x
      congr 1
      ring
    · congr 1
      ring

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:750published source at ed709a7f320d

No declaration docstring.

private theorem normed_bump_convolution_lipschitz {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (φ : ContDiffBump (0 : E)) :
    LipschitzWith L (φ.normed volume ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f) := by
  have hc := φ.hasCompactSupport_normed (μ := (volume : Measure E))
  have he := hc.convolutionExists_left (μ := (volume : Measure E)) (ContinuousLinearMap.lsmul ℝ ℝ)
    φ.continuous_normed hf.continuous.locallyIntegrable
  have hei (x : E) : Integrable (fun z => φ.normed volume z * f (x - z)) (volume : Measure E) := by
    simpa only [ConvolutionExistsAt, ContinuousLinearMap.lsmul_apply, smul_eq_mul] using he x
  apply LipschitzWith.of_dist_le_mul
  intro x y
  change ‖(∫ z, φ.normed volume z * f (x - z)) -
    (∫ z, φ.normed volume z * f (y - z))‖ ≤ (L : ℝ) * dist x y
  rw [← integral_sub (hei x) (hei y)]
  calc
    _ ≤ ∫ z, ‖φ.normed volume z * f (x - z) - φ.normed volume z * f (y - z)‖ :=
      norm_integral_le_integral_norm _
    _ ≤ ∫ z, φ.normed volume z * ((L : ℝ) * dist x y) := by
      apply integral_mono ((hei x).sub (hei y)).norm
        (φ.integrable_normed.mul_const _)
      intro z
      change ‖φ.normed volume z * f (x - z) - φ.normed volume z * f (y - z)‖ ≤ _
      rw [← mul_sub, norm_mul, Real.norm_eq_abs (φ.normed volume z),
        abs_of_nonneg (φ.nonneg_normed z)]
      apply mul_le_mul_of_nonneg_left _ (φ.nonneg_normed z)
      simpa only [dist_eq_norm, sub_sub_sub_cancel_right] using hf.dist_le_mul (x - z) (y - z)
    _ = _ := by rw [integral_mul_const, φ.integral_normed, one_mul]

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:766published source at ed709a7f320d

No declaration docstring.

private theorem normed_bump_convolution_error {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (φ : ContDiffBump (0 : E)) (x : E) :
    |(φ.normed volume ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f) x - f x| ≤
      (L : ℝ) * φ.rOut := by
  rw [← Real.norm_eq_abs, ← dist_eq_norm]
  apply φ.dist_normed_convolution_le hf.continuous.aestronglyMeasurable
  intro z hz
  exact (hf.dist_le_mul z x).trans
    (mul_le_mul_of_nonneg_left (Metric.mem_ball.mp hz).le L.coe_nonneg)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:793published source at ed709a7f320d

No declaration docstring.

private def approximationBump (n : ℕ) : ContDiffBump (0 : E) where
  rIn := ((1 / 2 : ℝ)^n) / 2
  rOut := (1 / 2 : ℝ)^n
  rIn_pos := by positivity
  rIn_lt_rOut := half_lt_self (by positivity)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:803published source at ed709a7f320d

No declaration docstring.

private def smoothApprox (f : E → ℝ) (n : ℕ) : E → ℝ :=
  (approximationBump n).normed volume ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:809published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_contDiff {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (n : ℕ) : ContDiff ℝ 1 (smoothApprox f n) := by
  exact (approximationBump n).hasCompactSupport_normed.contDiff_convolution_left
    (ContinuousLinearMap.lsmul ℝ ℝ) (approximationBump n).contDiff_normed
    hf.continuous.locallyIntegrable

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:812published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_lipschitz {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (n : ℕ) : LipschitzWith L (smoothApprox f n) :=
  normed_bump_convolution_lipschitz hf (approximationBump n)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:818published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_error {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (n : ℕ) (x : E) :
    |smoothApprox f n x - f x| ≤ (L : ℝ) * (1 / 2 : ℝ)^n :=
  normed_bump_convolution_error hf (approximationBump n) x

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:822published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_tendsto {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (x : E) :
    Filter.Tendsto (fun n => smoothApprox f n x) Filter.atTop (𝓝 (f x)) := by
  apply ContDiffBump.convolution_tendsto_right_of_continuous
    (φ := fun n => approximationBump (E := E) n) (μ := (volume : Measure E)) _ hf.continuous x
  exact tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:827published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_mean_error {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (n : ℕ) :
    |(∫ x, smoothApprox f n x ∂stdGaussian E) - (∫ x, f x ∂stdGaussian E)| ≤
      (L : ℝ) * (1 / 2 : ℝ)^n := by
  have hi := (integrable_and_integrable_exp_centered_of_lipschitz (μ := stdGaussian E) hf).1
  have hin := (integrable_and_integrable_exp_centered_of_lipschitz
    (μ := stdGaussian E) (smoothApprox_lipschitz hf n)).1
  rw [← integral_sub hin hi, ← Real.norm_eq_abs]
  have h := norm_integral_le_of_norm_le_const (μ := stdGaussian E)
    (f := fun x => smoothApprox f n x - f x) (C := (L : ℝ) * (1 / 2 : ℝ)^n)
    (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs] using smoothApprox_error hf n x)
  simpa using h

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:834published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_mean_tendsto {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) :
    Filter.Tendsto (fun n => ∫ x, smoothApprox f n x ∂stdGaussian E) Filter.atTop
      (𝓝 (∫ x, f x ∂stdGaussian E)) := by
  rw [tendsto_iff_norm_sub_tendsto_zero]
  have he : Filter.Tendsto (fun n : ℕ => (L : ℝ) * (1 / 2 : ℝ)^n) Filter.atTop (𝓝 0) := by
    simpa only [mul_zero] using
      (tendsto_pow_atTop_nhds_zero_of_lt_one
        (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num)).const_mul (L : ℝ)
  exact squeeze_zero (fun _ => norm_nonneg _) (fun n => by
    simpa only [Real.norm_eq_abs] using smoothApprox_mean_error hf n) he

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:847published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_centered_exp_bound {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t : ℝ) (n : ℕ) (x : E) :
    Real.exp (t * (smoothApprox f n x - ∫ z, smoothApprox f n z ∂stdGaussian E)) ≤
      Real.exp (2 * |t| * (L : ℝ)) * Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) := by
  let mn : ℝ := ∫ z, smoothApprox f n z ∂stdGaussian E
  let m : ℝ := ∫ z, f z ∂stdGaussian E
  have hrad : (L : ℝ) * (1 / 2 : ℝ)^n ≤ (L : ℝ) := by
    simpa only [mul_one] using mul_le_mul_of_nonneg_left
      (pow_le_one₀ (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num : (1 / 2 : ℝ) ≤ 1)) L.coe_nonneg
  have hx : |smoothApprox f n x - f x| ≤ (L : ℝ) := (smoothApprox_error hf n x).trans hrad
  have hm : |mn - m| ≤ (L : ℝ) := (smoothApprox_mean_error hf n).trans hrad
  have hc : |(smoothApprox f n x - mn) - (f x - m)| ≤ 2 * (L : ℝ) := by
    calc
      _ = |(smoothApprox f n x - f x) - (mn - m)| := by congr 1; ring
      _ ≤ |smoothApprox f n x - f x| + |mn - m| := abs_sub _ _
      _ ≤ _ := by linarith
  have hb : t * ((smoothApprox f n x - mn) - (f x - m)) ≤ 2 * |t| * (L : ℝ) := by
    calc
      _ ≤ |t * ((smoothApprox f n x - mn) - (f x - m))| := le_abs_self _
      _ = |t| * |(smoothApprox f n x - mn) - (f x - m)| := abs_mul _ _
      _ ≤ |t| * (2 * (L : ℝ)) := mul_le_mul_of_nonneg_left hc (abs_nonneg _)
      _ = _ := by ring
  rw [← Real.exp_add]
  apply Real.exp_le_exp.mpr
  change t * (smoothApprox f n x - mn) ≤ 2 * |t| * (L : ℝ) + t * (f x - m)
  nlinarith

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:859published source at ed709a7f320d

No declaration docstring.

private theorem smoothApprox_centered_exp_integral_tendsto {f : E → ℝ} {L : ℝ≥0}
    (hf : LipschitzWith L f) (t : ℝ) :
    Filter.Tendsto
      (fun n => ∫ x, Real.exp (t * (smoothApprox f n x - ∫ z, smoothApprox f n z ∂stdGaussian E))
        ∂stdGaussian E) Filter.atTop
      (𝓝 (∫ x, Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)) ∂stdGaussian E)) := by
  apply tendsto_integral_of_dominated_convergence
    (fun x => Real.exp (2 * |t| * (L : ℝ)) * Real.exp (t * (f x - ∫ z, f z ∂stdGaussian E)))
  · intro n
    have hcont := (smoothApprox_lipschitz hf n).continuous
    fun_prop
  · exact ((integrable_and_integrable_exp_centered_of_lipschitz
      (μ := stdGaussian E) hf).2 t).const_mul _
  · intro n
    filter_upwards with x
    rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
    exact smoothApprox_centered_exp_bound hf t n x
  · filter_upwards with x
    exact Real.continuous_exp.continuousAt.tendsto.comp
      (((smoothApprox_tendsto hf x).sub (smoothApprox_mean_tendsto hf)).const_mul t)

end GaussianDensity

/-- Sharp centered Laplace bound for the actual standard Gaussian, with all
domains and the smooth approximation produced internally. -/

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:886published source at ed709a7f320d

- Sharp centered Laplace bound for the actual standard Gaussian, with all domains and the smooth approximation produced internally.

theorem integral_exp_centered_le_stdGaussian_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂ProbabilityTheory.stdGaussian E))
      ∂ProbabilityTheory.stdGaussian E) ≤ Real.exp ((L : ℝ)^2 * t^2 / 2) := by
  by_cases hL : L = 0
  · subst L
    rw [centered_exp_integral_of_lipschitz_zero hf t]
    norm_num
  · rcases subsingleton_or_nontrivial E with hE | hE
    · letI : Subsingleton E := hE
      rw [centered_exp_integral_of_subsingleton f t]
      exact Real.one_le_exp_iff.mpr (by positivity)
    · exact le_of_tendsto' (smoothApprox_centered_exp_integral_tendsto hf t)
        (fun n => gaussian_centered_laplace_bound_c1
          (smoothApprox_contDiff hf n) (smoothApprox_lipschitz hf n) t)

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential
end

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianLipschitzExponential.lean:911published source at ed709a7f320dOpen detailed card