MeasureTheory.weaktype_estimate_truncCompl_top

lemma weaktype_estimate_truncCompl_top {C₀ : ℝ≥0} (hC₀ : 0 < C₀) {p p₀ q₀ : ℝ≥0∞}    (hp₀ : 0 < p₀) (hq₀ : q₀ = ⊤) (hp₀p : p₀ < p) (hp : p ≠ ⊤) {f : α → E₁'} (hf : MemLp f p μ)    (h₀T : HasWeakType T' p₀ q₀ μ ν C₀) (ht : 0 < t) {a : ℝ≥0∞} {d : ℝ≥0∞} -- (hd : 0 < d)    (ha : a = (t / d) ^ (p₀.toReal / (p₀.toReal - p.toReal)))    (hdeq : d = ((ENNReal.ofNNReal C₀) ^ p₀.toReal * eLpNorm f p μ ^ p.toReal) ^ p₀.toReal⁻¹) :    distribution (T' (truncCompl f a)) t ν = 0 := by  by_cases ht' : t = ∞  · simp [ht']  rcases (eq_zero_or_pos (eLpNormEssSup f μ)) with snorm_zero | snorm_pos  · have : eLpNorm (trnc ⊥ f a) ⊤ μ = 0 := by      apply nonpos_iff_eq_zero.mp      rw [← snorm_zero]      exact eLpNorm_trnc_est (p := ⊤)    have obs : eLpNorm (T' (trnc ⊥ f a)) ⊤ ν = 0 :=      weaktype_aux₀ p₀ ⊤ (hq₀ ▸ zero_lt_top) zero_lt_top h₀T hf.1.truncCompl this    exact nonpos_iff_eq_zero.mp      (Trans.trans (distribution_mono_right (Trans.trans obs zero_le)) meas_eLpNormEssSup_lt)  · have p_pos : 0 < p := hp₀.trans hp₀p    have snorm_p_pos : eLpNorm f p μ ≠ 0 := by      intro snorm_0      have := hf.1      have : eLpNormEssSup f μ = 0 := by        rw [← eLpNorm_exponent_top]        exact eLpNorm_eq_zero_of_eLpNorm_eq_zero hf.1 p_pos.ne' snorm_0      exact snorm_pos.ne' this    have term_pos : (ENNReal.ofNNReal C₀) ^ p₀.toReal * eLpNorm f p μ ^ p.toReal > 0 := by      apply ENNReal.mul_pos <;> exact (rpow_pos_of_nonneg (by positivity) (by positivity)).ne'    have d_pos : 0 < d := hdeq ▸ ENNReal.rpow_pos term_pos (by finiteness)    have d_ne_top : d ≠ ⊤ := hdeq ▸ (by finiteness)    have a_pos : 0 < a := ha ▸ ENNReal.rpow_pos (ENNReal.div_pos ht.ne' d_ne_top) (by finiteness)    have obs : MemLp (truncCompl f a) p₀ μ := truncCompl_Lp_Lq_lower hp ⟨hp₀, hp₀p.le⟩ a_pos hf    have wt_est := (h₀T (truncCompl f a) obs).2    unfold wnorm at wt_est    split_ifs at wt_est    have snorm_est : eLpNormEssSup (T' (truncCompl f a)) ν ≤ t := by      apply le_of_rpow_le (exp_toReal_pos hp₀ hp₀p.ne_top)      calc      _ ≤ (↑C₀ * eLpNorm (truncCompl f a) p₀ μ) ^ p₀.toReal := by gcongr      _ ≤ (↑C₀) ^ p₀.toReal * ((a ^ (p₀.toReal - p.toReal)) *          eLpNorm f p μ ^ p.toReal) := by        rw [ENNReal.mul_rpow_of_nonneg _ _ toReal_nonneg]        gcongr        exact estimate_eLpNorm_truncCompl hp ⟨hp₀, hp₀p.le⟩ hf.1 a_pos      _ = (↑C₀) ^ p₀.toReal * eLpNorm f p μ ^ p.toReal * (d ^ p₀.toReal)⁻¹ * (t ^ p₀.toReal) := by        rw [ha, ← ENNReal.rpow_mul, div_mul_cancel₀]        · -- FIXME: can/should this be shared with the lemma below?          rw [ENNReal.div_rpow_of_nonneg, div_eq_mul_inv] <;> try positivity          ring        · exact (sub_neg.mpr (toReal_strict_mono hp hp₀p)).ne      _ = _ := by        nth_rw 2 [← one_mul (t ^ p₀.toReal)]        rw [hdeq, ENNReal.rpow_inv_rpow, ENNReal.mul_inv_cancel (by positivity) (by finiteness)]        exact toReal_ne_zero.mpr ⟨hp₀.ne', by finiteness⟩    apply nonpos_iff_eq_zero.mp    calc    _ ≤ distribution (T' (truncCompl f a)) (eLpNormEssSup (T' (truncCompl f a)) ν) ν :=      distribution_mono_right snorm_est    _ = _ := meas_eLpNormEssSup_lt