prod — Mathlib

English

See MemLp.prod for the applied version: the product of functions under MemLp yields a MemLp with adjusted exponent.

Русский

См. MemLp.prod для примененного варианта: произведение функций в MemLp дает MemLp с новым показателем.

LaTeX

$$MemLp.prod hf$$

Lean4

/-- See `MemLp.prod'` for the applied version. -/
protected theorem prod (hf : ∀ i ∈ s, MemLp (f i) (p i) μ) : MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ := by
  induction s using cons_induction with
  | empty => by_cases hμ : μ = 0 <;> simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
  | cons i s hi ih =>
    rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

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