hasFiniteIntegral_of_dominated_convergence_enorm

English

If bound has finite integral and h_bound/h_lim hold, then HasFiniteIntegral f' μ.

Русский

При условии конечного интеграла bound и выполнении условий h_bound, h_lim, имеет место HasFiniteIntegral f' μ.

LaTeX

$$$HasFiniteIntegral bound μ \land (\forall n, \forallᵐ a, \|F'n a\| ≤ bound a) \land (\forallᵐ a, Tendsto (F'n a) atTop (nhds f'a)) \Rightarrow HasFiniteIntegral f' μ$$$

Lean4

theorem hasFiniteIntegral_of_dominated_convergence_enorm (bound_hasFiniteIntegral : HasFiniteIntegral bound' μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F' n a‖ₑ ≤ bound' a) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))) :
    HasFiniteIntegral f' μ := by
  /- `‖F' n a‖ₑ ≤ bound' a` and `‖F' n a‖ₑ --> ‖f' a‖ₑ` implies `‖f a‖ₑ ≤ bound' a`,
      and so `∫ ‖f'‖ₑ ≤ ∫ bound' < ∞` since `bound'` has finite integral -/

  rw [hasFiniteIntegral_iff_enorm]
  calc
    (∫⁻ a, ‖f' a‖ₑ ∂μ) ≤ ∫⁻ a, bound' a ∂μ := lintegral_mono_ae <| ae_enorm_le_bound h_bound h_lim
    _ < ∞ := bound_hasFiniteIntegral

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