MeasureTheory.weaktype_estimate_trunc_top_top

lemma weaktype_estimate_trunc_top_top {a : ℝ≥0∞} {C₁ : ℝ≥0}    (hC₁ : 0 < C₁) {p p₁ q₁ : ℝ≥0∞} (hp : 0 < p)    (hp₁ : p₁ = ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p ≤ p₁) {f : α → E₁'} (hf : MemLp f p μ)    (h₁T : HasWeakType T' p₁ q₁ μ ν C₁) (ha : a = t / C₁) :    distribution (T' (trunc f a)) t ν = 0 := by  by_cases ht : t = ⊤  · simp [ht]  rw [ha]  have obs : MemLp (trunc f (t / C₁)) p₁ μ := trunc_Lp_Lq_higher ⟨hp, hp₁p⟩ hf (by finiteness)  have wt_est := (h₁T (trunc f (t / C₁)) obs).2  simp only [wnorm, eLpNorm, hq₁, ↓reduceIte, hp₁, top_ne_zero] at wt_est  apply nonpos_iff_eq_zero.mp  have ineq : eLpNormEssSup (T' (trunc f (t / C₁))) ν ≤ t := calc    _ ≤ C₁ * eLpNormEssSup (trunc f (t / C₁)) μ := wt_est    _ ≤ C₁ * (max 0 (t / C₁)) := by      gcongr      exact trunc_eLpNormEssSup_le _    _ ≤ _ := by      rw [max_eq_right zero_le,        ENNReal.mul_div_cancel (ENNReal.coe_ne_zero.mpr hC₁.ne') (by finiteness)]  calc  _ ≤ distribution (T' (trunc f (t / C₁))) (eLpNormEssSup (T' (trunc f (t / C₁))) ν) ν :=      distribution_mono_right ineq  _ = 0 := distribution_eLpNormEssSup