Source indexedlemma · leanprover/lean4:v4.32.0

le_localOscillation

Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:211 to 218

Mathematical statement

Exact Lean statement

lemma le_localOscillation [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X}
    (hy : y ∈ ball x r) (hz : z ∈ ball x r) : ‖coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g z‖ ≤
    ENNReal.toReal (localOscillation (ball x r) (coeΘ f) (coeΘ g))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma le_localOscillation [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X}    (hy : y ∈ ball x r) (hz : z ∈ ball x r) : ‖coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g z‖ ≤    ENNReal.toReal (localOscillation (ball x r) (coeΘ f) (coeΘ g)) := by  rw [(ENNReal.toReal_ofReal (norm_nonneg _)).symm]  let f (z) := ⨆ (_ : z ∈ ball x r ×ˢ ball x r), ENNReal.ofReal ‖f z.1 - g z.1 - f z.2 + g z.2‖  apply ENNReal.toReal_mono  · exact lt_of_le_of_lt CompatibleFunctions.localOscillation_le_cdist ENNReal.ofReal_lt_top |>.ne  · exact le_of_eq_of_le (Eq.symm (iSup_pos ⟨hy, hz⟩)) (le_iSup f ⟨y, z⟩)