Source indexedlemma · leanprover/lean4:v4.32.0

lowerSemicontinuous_simpleNontangentialOperator

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:701 to 712

Source documentation

Part of Lemma 10.1.6.

Exact Lean statement

lemma lowerSemicontinuous_simpleNontangentialOperator {g : X → ℂ} :
    LowerSemicontinuous (simpleNontangentialOperator K r g)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lowerSemicontinuous_simpleNontangentialOperator {g : X → ℂ} :    LowerSemicontinuous (simpleNontangentialOperator K r g) := by  unfold simpleNontangentialOperator  simp_rw [lowerSemicontinuous_iff_isOpen_preimage, preimage, mem_Ioi, lt_iSup_iff, ← iUnion_setOf,    mem_ball_comm, exists_prop]  intro y  apply isOpen_iUnion; intro R  apply isOpen_iUnion; intro hR  apply isOpen_iUnion; intro x'  by_cases hx' : y < ‖czOperator K R g x'‖ₑ  · simp_rw [hx', and_true, setOf_mem_eq, isOpen_ball]  · simp [hx']