lintegral_rpow_funMulInvSnorm_eq_one

English

If ∫ f^p ≠ 0 and ∫ f^p ≠ ∞, then ∫ (funMulInvSnorm f p μ)^p = 1.

Русский

Если ∫ f^p не равно нулю и не бесконечно, то ∫ (funMulInvSnorm f p μ)^p = 1.

LaTeX

$$$\\int⁻ c, (funMulInvSnorm f p μ c)^p ∂μ = 1$$$

Lean4

theorem lintegral_rpow_funMulInvSnorm_eq_one {p : ℝ} (hp0_lt : 0 < p) {f : α → ℝ≥0∞}
    (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) : ∫⁻ c, funMulInvSnorm f p μ c ^ p ∂μ = 1 :=
  by
  simp_rw [funMulInvSnorm_rpow hp0_lt]
  rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]
  rwa [inv_ne_top]

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