comp_fst — Mathlib

English

For NNReal p>0, eLpNorm equals the lintegral with exponent p.toReal.

Русский

Для p>0 в NNReal имеем eLpNorm f p μ = (∫⁻ ‖f‖^{p.toReal} dμ)^{1/p.toReal}.

LaTeX

$$$eLpNorm\\,f\\,p\\,\\mu = \\left(\\int^{-} a\\; \\|f(a)\\|_{\\varepsilon}^{\\,p.toReal} \\partial\\mu(a)\\right)^{1/p.toReal}$$$

Lean4

theorem comp_fst {f : α → ε} (hf : MemLp f p μ) (ν : Measure β) [IsFiniteMeasure ν] :
    MemLp (fun x ↦ f x.1) p (μ.prod ν) :=
  by
  have hf' : MemLp f p (ν .univ • μ) := hf.smul_measure (by simp)
  change MemLp (f ∘ Prod.fst) p (μ.prod ν)
  rw [← memLp_map_measure_iff ?_ (by fun_prop)]
  · simpa using hf'
  · simpa using hf'.1

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