BST_LNT_of_BST_NT

lemma BST_LNT_of_BST_NT {Q : SimpleFunc X (Θ X)}    (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)) :    ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)      2 2 volume volume (C_Ts a) := fun θ f bf ↦ by  constructor  · exact lowerSemicontinuous_LNT.measurable.aestronglyMeasurable  · refine (eLpNorm_mono_enorm fun x ↦ ?_).trans (hT f bf).2    simp_rw [enorm_eq_self]    refine iSup_le fun R₂ ↦ iSup₂_le fun R₁ mR₁ ↦ iSup₂_le fun x' mx' ↦ ?_    rw [min_def]; split_ifs with h    · trans ⨆ R₁ ∈ Ioo 0 R₂, ⨆ x' ∈ ball x R₁, ‖∫ y in Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ; swap      · apply le_iSup _ R₂      trans ⨆ x' ∈ ball x R₁, ‖∫ y in Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ; swap      · apply le_iSup₂ _ mR₁      rw [EAnnulus.oo_eq_annulus mR₁.1.le]      apply le_iSup₂ _ mx'    · rcases le_or_gt (upperRadius Q θ x') (ENNReal.ofReal R₁) with hur | hur      · rw [EAnnulus.oo_eq_empty hur, setIntegral_empty, enorm_zero]; exact zero_le      rw [not_le] at h      have urnt : upperRadius Q θ x' ≠ ⊤ := by        rw [← lt_top_iff_ne_top]; exact h.trans (by finiteness)      rw [← ofReal_toReal urnt] at h hur ⊢      rw [ofReal_lt_ofReal_iff (mR₁.1.trans mR₁.2)] at h      rw [ofReal_lt_ofReal_iff_of_nonneg mR₁.1.le] at hur      rw [EAnnulus.oo_eq_annulus mR₁.1.le]; set R := (upperRadius Q θ x').toReal      trans ⨆ R₁ ∈ Ioo 0 R, ⨆ x' ∈ ball x R₁, ‖∫ y in Annulus.oo x' R₁ R, K x' y * f y‖ₑ; swap      · convert! le_iSup _ R; rfl      trans ⨆ x' ∈ ball x R₁, ‖∫ y in Annulus.oo x' R₁ R, K x' y * f y‖ₑ; swap      · have : R₁ ∈ Ioo 0 R := ⟨mR₁.1, hur⟩        apply le_iSup₂ _ this      apply le_iSup₂ _ mx'