norm_condExpIndL1_le — Mathlib

English

For every x in G, the Lp-condExpIndL1 is bounded in norm by the measure of S times the norm of x: ||condExpIndL1 hm μ s x|| ≤ μ.real(s) · ||x||.

Русский

Для каждого x ∈ G норма condExpIndL1 hm μ s x ограничена: ∥condExpIndL1 hm μ s x∥ ≤ μ.real(s) · ∥x∥.

LaTeX

$$$ \| condExpIndL1\; hm\; \mu\; s\; x \| \leq \mu.real\; s\; \|x\|, \quad x \in G,$$

Lean4

theorem norm_condExpIndL1_le (x : G) : ‖condExpIndL1 hm μ s x‖ ≤ μ.real s * ‖x‖ :=
  by
  by_cases hs : MeasurableSet s
  swap
  · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [Lp.norm_zero]
    exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)
  by_cases hμs : μ s = ∞
  · rw [condExpIndL1_of_measure_eq_top hμs x, Lp.norm_zero]
    exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)
  · rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x]
    exact norm_condExpIndL1Fin_le hs hμs x

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