Source indexedlemma · leanprover/lean4:v4.32.0

continuous_of_iHolENorm_ne_top'

Carleson.HolderNorm · Carleson/HolderNorm.lean:73 to 84

Mathematical statement

Exact Lean statement

lemma continuous_of_iHolENorm_ne_top' (ht : 0 < t) (hφ : support φ ⊆ ball z R)
    (h'φ : iHolENorm φ z (2 * R) t ≠ ∞) :
    Continuous φ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuous_of_iHolENorm_ne_top' (ht : 0 < t) (hφ : support φ ⊆ ball z R)    (h'φ : iHolENorm φ z (2 * R) t ≠ ∞) :    Continuous φ := by  rcases le_or_gt R 0 with hR | hR  · have : support φ ⊆ ∅ := by rwa [ball_eq_empty.2 hR] at hφ    simp only [subset_empty_iff, support_eq_empty_iff] at this    simp only [this]    exact continuous_const  apply HolderOnWith.of_iHolENorm_ne_top ht.le h'φ |>.continuousOn (by simp [ht])    |>.continuous_of_tsupport_subset isOpen_ball  apply (closure_mono hφ).trans (closure_ball_subset_closedBall.trans ?_)  exact closedBall_subset_ball (by linarith)