CubicPathwidth.T2.SlepianStein

Source file CubicPathwidth/T2/SlepianStein.lean of the Lean project (how it is built).

import CubicPathwidth.T2.Defs

/-!
# Gaussian integration by parts (Stein's identity) for Slepian's inequality

* `stein_one`: for the standard normal law, `E[s g(s)] = E[g'(s)]` when `g` is bounded and
  differentiable everywhere with bounded derivative;
* `stein_coord`: the same identity in one coordinate of the product of standard normal laws on
  `Fin (n + 1) → ℝ`.
-/

noncomputable section
open scoped Real
open MeasureTheory ProbabilityTheory Set Filter Topology

namespace CubicPathwidth
namespace T2
namespace Slepian

/-- Product of standard normal laws on `Fin N → ℝ`. -/
abbrev gpi (N : ℕ) : Measure (Fin N → ℝ) := Measure.pi fun _ : Fin N => gaussianReal 0 1

/-- Standard normal density. -/
abbrev sphi (x : ℝ) : ℝ := gaussianPDFReal 0 1 x

theorem sphi_eq (x : ℝ) : sphi x = (Real.sqrt (2 * π))⁻¹ * Real.exp (-x ^ 2 / 2) := by
  simp [sphi, gaussianPDFReal]

theorem hasDerivAt_sphi (x : ℝ) : HasDerivAt sphi (-x * sphi x) x := by
  have h1 : HasDerivAt (fun x : ℝ => -x ^ 2 / 2) (-x) x :=
    ((hasDerivAt_pow 2 x).neg.div_const 2).congr_deriv (by push_cast; ring)
  have h2 := (h1.exp).const_mul ((Real.sqrt (2 * π))⁻¹)
  have e : sphi = fun y => (Real.sqrt (2 * π))⁻¹ * Real.exp (-y ^ 2 / 2) := funext sphi_eq
  rw [e]
  convert h2 using 1
  ring

theorem integrable_sphi : Integrable sphi := integrable_gaussianPDFReal 0 1

theorem continuous_sphi : Continuous sphi := by
  unfold sphi gaussianPDFReal
  fun_prop

theorem integrable_mul_sphi : Integrable fun x => x * sphi x := by
  have h := (integrable_mul_exp_neg_mul_sq (b := 1 / 2) (by norm_num)).const_mul
    ((Real.sqrt (2 * π))⁻¹)
  refine h.congr (ae_of_all _ fun x => ?_)
  simp only [sphi_eq]
  have : -(1 / 2) * x ^ 2 = -x ^ 2 / 2 := by ring
  rw [this]; ring

/-- One-dimensional Stein identity. -/
theorem stein_one {g g' : ℝ → ℝ} (hd : ∀ s, HasDerivAt g (g' s) s) {C C' : ℝ}
    (hb : ∀ s, |g s| ≤ C) (hb' : ∀ s, |g' s| ≤ C') :
    ∫ s, s * g s ∂gaussianReal 0 1 = ∫ s, g' s ∂gaussianReal 0 1 := by
  rw [integral_gaussianReal_eq_integral_smul one_ne_zero,
    integral_gaussianReal_eq_integral_smul one_ne_zero]
  simp only [smul_eq_mul]
  have hgc : Continuous g := continuous_iff_continuousAt.2 fun s => (hd s).continuousAt
  have hg'm : Measurable g' := by
    have : g' = deriv g := funext fun s => (hd s).deriv.symm
    rw [this]; exact measurable_deriv g
  have key := integral_mul_deriv_eq_deriv_mul_of_integrable (u := g) (u' := g')
    (v := fun s => -sphi s) (v' := fun s => s * sphi s)
    (fun x _ => hd x) (fun x _ => by
      have := (hasDerivAt_sphi x).neg
      convert this using 1; ring)
    (integrable_mul_sphi.bdd_mul hgc.aestronglyMeasurable
      (ae_of_all _ fun s => by simpa using hb s))
    (integrable_sphi.neg.bdd_mul hg'm.aestronglyMeasurable
      (ae_of_all _ fun s => by simpa using hb' s))
    (integrable_sphi.neg.bdd_mul hgc.aestronglyMeasurable
      (ae_of_all _ fun s => by simpa using hb s))
  simp only [mul_neg, integral_neg, neg_neg] at key
  calc ∫ s, sphi s * (s * g s) = ∫ s, g s * (s * sphi s) :=
        integral_congr_ae (ae_of_all _ fun s => by ring)
    _ = ∫ s, g' s * sphi s := key
    _ = ∫ s, sphi s * g' s := integral_congr_ae (ae_of_all _ fun s => by ring)

theorem integrable_coord (N : ℕ) (j : Fin N) : Integrable (fun x : Fin N → ℝ => x j) (gpi N) :=
  integrable_eval IsGaussian.integrable_id

/-- Stein identity in one coordinate of `gpi (n + 1)`. -/
theorem stein_coord {n : ℕ} (j : Fin (n + 1)) {H H' : (Fin (n + 1) → ℝ) → ℝ}
    (hH : Continuous H) (hH' : Measurable H') {C C' : ℝ} (hb : ∀ x, |H x| ≤ C)
    (hb' : ∀ x, |H' x| ≤ C')
    (hd : ∀ x, HasDerivAt (fun s => H (Function.update x j s)) (H' x) (x j)) :
    ∫ x, x j * H x ∂gpi (n + 1) = ∫ x, H' x ∂gpi (n + 1) := by
  have hp := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => gaussianReal 0 1) j
  set e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) => ℝ) j
  have hps := hp.symm
  rw [← hps.integral_comp' (fun x => x j * H x), ← hps.integral_comp' H']
  have hint1 : Integrable (fun x : Fin (n + 1) → ℝ => x j * H x) (gpi (n + 1)) :=
    (integrable_coord _ j).mul_bdd hH.aestronglyMeasurable
      (ae_of_all _ fun x => by simpa using hb x)
  have hint2 : Integrable H' (gpi (n + 1)) :=
    Integrable.of_bound hH'.aestronglyMeasurable C' (ae_of_all _ fun x => by simpa using hb' x)
  have i1 := (hps.integrable_comp_emb e.symm.measurableEmbedding).2 hint1
  have i2 := (hps.integrable_comp_emb e.symm.measurableEmbedding).2 hint2
  rw [integral_prod_symm (fun p => e.symm p j * H (e.symm p)) i1,
    integral_prod_symm (fun p => H' (e.symm p)) i2]
  refine integral_congr_ae (ae_of_all _ fun z => ?_)
  have he : ∀ s, e.symm (s, z) = Fin.insertNth j s z := fun s => rfl
  simp only [he, Fin.insertNth_apply_same]
  refine stein_one (g := fun s => H (Fin.insertNth j s z)) (fun s => ?_)
    (fun s => hb _) (fun s => hb' _)
  have := hd (Fin.insertNth j s z)
  simp only [Fin.insertNth_apply_same, Fin.update_insertNth] at this
  exact this

end Slepian
end T2
end CubicPathwidth
Back to top