comp_snd — Mathlib

English

If f ∈ MemLp(p,μ) on α,β, then the first-coordinate projection f∘Prod.fst ∈ MemLp(p,μ×ν) when ν is finite.

Русский

Если f ∈ MemLp(p,μ) на α,β, то f∘Prod.fst ∈ MemLp(p,μ×ν), когда ν конечно-мера.

LaTeX

$$$\\operatorname{MemLp}\\left(f\\circ \\mathrm{Prod.fst}\\right)\\,p\\, (\\mu\\times\\nu)$$$

Lean4

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

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