eLpNormEssSup_indicator_const_eq — Mathlib

English

If s is measurable, the essSup of the indicator of a constant c equals the norm of c.

Русский

Если s измеримо, essSup индикатора константы c равен норме c.

LaTeX

$$$eLpNormEssSup (s.indicator (fun _ => c)) μ = \|c\|_ε$$$

Lean4

theorem eLpNormEssSup_indicator_const_eq (s : Set α) (c : ε) (hμs : μ s ≠ 0) :
    eLpNormEssSup (s.indicator fun _ : α => c) μ = ‖c‖ₑ :=
  by
  refine le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_
  by_contra! h
  have h' := ae_iff.mp (ae_lt_of_essSup_lt h)
  push_neg at h'
  refine hμs (measure_mono_null (fun x hx_mem => ?_) h')
  rw [Set.mem_setOf_eq, Set.indicator_of_mem hx_mem]

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