Source indexedlemma · leanprover/lean4:v4.32.0

lowerSemicontinuous_LNT

Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:159 to 168

Mathematical statement

Exact Lean statement

lemma lowerSemicontinuous_LNT {Q : SimpleFunc X (Θ X)} {θ : Θ X} :
    LowerSemicontinuous (linearizedNontangentialOperator Q θ K f)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lowerSemicontinuous_LNT {Q : SimpleFunc X (Θ X)} {θ : Θ X} :    LowerSemicontinuous (linearizedNontangentialOperator Q θ K f) := by  unfold linearizedNontangentialOperator  simp_rw [lowerSemicontinuous_iff_isOpen_preimage, preimage, mem_Ioi, lt_iSup_iff, ← iUnion_setOf,    exists_prop]  refine fun M ↦ isOpen_iUnion fun R₂ ↦ isOpen_biUnion fun R₁ hR₁ ↦ isOpen_iUnion fun x' ↦ ?_  by_cases hx' : M < ‖∫ y in EAnnulus.oo x' (ENNReal.ofReal R₁)      (min (ENNReal.ofReal R₂) (upperRadius Q θ x')), K x' y * f y‖ₑ  · simp_rw [hx', and_true, mem_ball_comm, setOf_mem_eq, isOpen_ball]  · simp [hx']