integrable_exp_sq_of_conv_neg — Mathlib

English

If exp(C ||x||^2) is integrable with respect to the convolved Gaussian μ ∗ (μ.map(−id)), then for every C′ < C, exp(C′ ||x||^2) is integrable with respect to μ.

Русский

Если экспонента с параметром C является интегрируемой по скрещённому гауссову распределению, то для любого C′ < C экспонента с C′ интегрируема по μ.

LaTeX

$$$\\exists C>0\\, Integrable(e^{C\\|x\\|^2},\\ μ∗(μ\\circ(-\\mathrm{Id}))) \\Rightarrow (\\forall C'

Lean4

/-- If `x ↦ exp (C * ‖x‖ ^ 2)` is integrable with respect to the centered Gaussian
`μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ))`, then for all `C' < C`, `x ↦ exp (C' * ‖x‖ ^ 2)`
is integrable with respect to `μ`. -/
theorem integrable_exp_sq_of_conv_neg (μ : Measure E) [IsGaussian μ] {C C' : ℝ}
    (hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ)))) (hC'_pos : 0 < C')
    (hC'_lt : C' < C) : Integrable (fun x ↦ rexp (C' * ‖x‖ ^ 2)) μ :=
  by
  have h_int : ∀ᵐ y ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ :=
    by
    rw [integrable_conv_iff (by fun_prop)] at hint
    replace hC := hint.1
    simp only [ContinuousLinearEquiv.coe_neg] at hC
    filter_upwards [hC] with y hy
    rw [integrable_map_measure (by fun_prop) (by fun_prop)] at hy
    convert hy with x
    simp only [Function.comp_apply, Pi.neg_apply, id_eq, Real.exp_eq_exp, mul_eq_mul_left_iff, norm_nonneg, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_left_inj₀]
    left
    simp_rw [← sub_eq_add_neg, norm_sub_rev]
  obtain ⟨y, hy⟩ : ∃ y, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ := h_int.exists
  let ε := (C - C') / C'
  have hε : 0 < ε := div_pos (by rwa [sub_pos]) (by positivity)
  suffices ∀ x, rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)
    by
    refine
      integrable_of_le_of_le (g₁ := 0) (g₂ := fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)) (by fun_prop) ?_
        ?_ (integrable_const _) (hy.const_mul _)
    · exact ae_of_all _ fun _ ↦ by positivity
    · exact ae_of_all _ this
  intro x
  rw [← Real.exp_add]
  gcongr -- `⊢ C' * ‖x‖ ^ 2 ≤ C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2` with `ε = (C - C') / C'`

  have h_le : ‖x‖ ^ 2 ≤ (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2 := by
    calc
      ‖x‖ ^ 2
      _ = ‖x - y + y‖ ^ 2 := by simp
      _ ≤ (‖x - y‖ + ‖y‖) ^ 2 := by grw [norm_add_le (x - y) y]
      _ = ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + 2 * ‖x - y‖ * ‖y‖ := by ring
      _ ≤ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + ε * ‖x - y‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2 :=
        by
        simp_rw [add_assoc]
        gcongr
        exact two_mul_le_add_mul_sq (by positivity)
      _ = (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2 := by ring
  calc
    C' * ‖x‖ ^ 2
    _ ≤ C' * ((1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2) := by gcongr
    _ = (C' * (1 + 1 / ε)) * ‖y‖ ^ 2 + (C' * (1 + ε)) * ‖x - y‖ ^ 2 := by ring
    _ = C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2 := by
      unfold ε
      congr 2
      · simp only [one_div, inv_div]
        rw [one_add_div (by rw [sub_ne_zero]; exact hC'_lt.ne'), div_div_eq_mul_div]
        simp only [sub_add_cancel]
        ring
      · rw [one_add_div (by positivity)]
        simp only [add_sub_cancel]
        rw [mul_div_cancel₀ _ (by positivity)]

Похожие утверждения