Source indexedlemma · leanprover/lean4:v4.32.0

iLipENorm_le_add

Carleson.LipschitzNorm · Carleson/LipschitzNorm.lean:46 to 61

Mathematical statement

Exact Lean statement

lemma iLipENorm_le_add (h : ∀ x ∈ ball z R, ‖φ x‖ ≤ C)
    (h' : ∀ x ∈ ball z R, ∀ x' ∈ ball z R, x ≠ x' → ‖φ x - φ x'‖ ≤ C' * dist x x' / R) :
    iLipENorm φ z R ≤ C + C'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma iLipENorm_le_add (h : ∀ x ∈ ball z R, ‖φ x‖ ≤ C)    (h' : ∀ x ∈ ball z R, ∀ x' ∈ ball z R, x ≠ x' → ‖φ x - φ x'‖ ≤ C' * dist x x' / R) :    iLipENorm φ z R ≤ C + C' := by  apply add_le_add  · simp only [iSup_le_iff, enorm_le_coe]    exact h  · apply ENNReal.mul_le_of_le_div'    simp only [ne_eq, iSup_le_iff]    intro x hx x' hx' hne    have hR : 0 < R := pos_of_mem_ball hx    have W := h' x hx x' hx' hne    rw [ENNReal.div_le_iff (by simpa only [ne_eq, edist_eq_zero] using hne) (edist_ne_top x x')]    convert ENNReal.ofReal_le_ofReal W    · exact (ofReal_norm (φ x - φ x')).symm    · rw [ENNReal.ofReal_div_of_pos hR, ENNReal.ofReal_mul NNReal.zero_le_coe, edist_dist,        ENNReal.mul_div_right_comm, ENNReal.ofReal_coe_nnreal]