fun_eq_funMulInvSnorm_mul_eLpNorm

English

The normalization identity for funMulInvSnorm: f(a) = funMulInvSnorm(f, p, μ)(a) · (∫ f^p dμ)^(1/p).

Русский

Идентичность нормализации для funMulInvSnorm: f(a) = funMulInvSnorm(f,p,μ)(a) · (∫ f^p dμ)^(1/p).

LaTeX

$$$f(a) = \\mathrm{funMulInvSnorm}(f,p,μ)(a) \\cdot (\\int⁻ c, f(c)^p ∂μ)^{1/p}$$$

Lean4

theorem fun_eq_funMulInvSnorm_mul_eLpNorm {p : ℝ} (f : α → ℝ≥0∞) (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0)
    (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) {a : α} : f a = funMulInvSnorm f p μ a * (∫⁻ c, f c ^ p ∂μ) ^ (1 / p) := by
  simp [funMulInvSnorm, mul_assoc, ENNReal.inv_mul_cancel, hf_nonzero, hf_top]

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