Source indexedlemma · leanprover/lean4:v4.32.0

eLpNormEssSup_nnreal_eq_iSup_nnreal

Carleson.ToMathlib.Topology.ContinuousOn · Carleson/ToMathlib/Topology/ContinuousOn.lean:62 to 74

Mathematical statement

Exact Lean statement

lemma eLpNormEssSup_nnreal_eq_iSup_nnreal {f : ℝ≥0∞ → ℝ≥0∞}
  (hf : ∀ (a : ℝ≥0∞) (x : ℝ≥0), a < f x → ContinuousWithinAt f (Set.Ioi ↑x) ↑x) :
    eLpNormEssSup (fun t : ℝ≥0 ↦ f t) volume = ⨆ (x : ℝ≥0), f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNormEssSup_nnreal_eq_iSup_nnreal {f : ℝ≥0∞ → ℝ≥0∞}  (hf : ∀ (a : ℝ≥0∞) (x : ℝ≥0), a < f x → ContinuousWithinAt f (Set.Ioi ↑x) ↑x) :    eLpNormEssSup (fun t : ℝ≥0 ↦ f t) volume = ⨆ (x : ℝ≥0), f x := by  symm  apply iSup_eq_essSup  intro x a ha  apply ContinuousWithinAt.measure_lt_ne_zero (x := x) (μ := volume) (by simp) _ ha  have : ContinuousWithinAt ENNReal.ofNNReal Set.univ x := by    fun_prop  convert! ContinuousWithinAt.comp_inter_of_eq (g := f) (hf a x ha) this rfl  simp only [Set.univ_inter]  ext y  simp