Source indexedlemma · leanprover/lean4:v4.32.0

lowerSemicontinuous_nontangentialOperator

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:1023 to 1034

Source documentation

Part of Lemma 10.1.6.

Exact Lean statement

lemma lowerSemicontinuous_nontangentialOperator {g : X → ℂ} :
    LowerSemicontinuous (nontangentialOperator K g)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lowerSemicontinuous_nontangentialOperator {g : X → ℂ} :    LowerSemicontinuous (nontangentialOperator K g) := by  unfold nontangentialOperator  simp_rw [lowerSemicontinuous_iff_isOpen_preimage, preimage, mem_Ioi, lt_iSup_iff, ← iUnion_setOf,    exists_prop]  intro M  apply isOpen_iUnion; intro R₂  apply isOpen_biUnion; intro R₁ hR₁  apply isOpen_iUnion; intro x'  by_cases hx' : M < ‖∫ (y : X) in Annulus.oo x' R₁ R₂, K x' y * g y‖ₑ  · simp_rw [hx', and_true, mem_ball_comm, setOf_mem_eq, isOpen_ball]  · simp [hx']