MeasureTheory.weaktype_estimate_trunc_top

lemma weaktype_estimate_trunc_top {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₁) (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' (trunc f a)) t ν = 0 := by  have := hf.1  by_cases ht' : t = ∞  · simp [ht']  have ha' : a ≠ ⊤ := by    have := MemLp.eLpNorm_lt_top hf    apply ha ▸ rpow_ne_top_of_ne_zero    · exact ENNReal.div_ne_zero.mpr ⟨ht.ne', hdeq ▸ by finiteness⟩    finiteness  have obs : MemLp (trunc f a) p₁ μ := trunc_Lp_Lq_higher ⟨hp, hp₁p.le⟩ hf ha'  have wt_est := (h₁T (trunc f a) obs).2  unfold wnorm at wt_est  split_ifs at wt_est  have hp₁' : p₁.toReal ≠ 0 := (toReal_pos (hp.trans hp₁p).ne' hp₁.ne_top).ne'  have : eLpNormEssSup (T' (trunc f a)) ν ^ p₁.toReal ≤      (C₁ * eLpNorm (trunc f a) p₁ μ) ^ p₁.toReal := by gcongr  have snorm_est : eLpNormEssSup (T' (trunc f a)) ν ≤ t := by    apply le_of_rpow_le (exp_toReal_pos (hp.trans hp₁p) hp₁.ne_top)    refine le_trans this ?_    rcases (eq_zero_or_pos (eLpNormEssSup f μ)) with snorm_zero | snorm_pos    · gcongr      calc      _ ≤ (ENNReal.ofNNReal C₁) * eLpNorm f p₁ μ := by        gcongr        apply eLpNorm_mono_enorm (fun x ↦ trunc_le_func)      _ ≤ _ := by        have : eLpNorm f p₁ μ = 0 := eLpNorm_eq_zero_of_eLpNormEssSup_eq_zero hf.1 snorm_zero        simp only [this, mul_zero, zero_le]    · have snorm_p_pos : eLpNorm f p μ ≠ 0 := by        by_contra snorm_0        exact snorm_pos.ne' <|            eLpNormEssSup_eq_zero_of_eLpNorm_eq_zero hf.1 hp.ne' snorm_0      -- XXX: these lines are the same as in the lemma above      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'      calc      _ ≤ ↑C₁ ^ p₁.toReal * (((a ^ (p₁.toReal - p.toReal))) * eLpNorm f p μ ^ p.toReal) := by        rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity)]        gcongr        exact estimate_eLpNorm_trunc hp₁.ne_top ⟨hp, hp₁p.le⟩ hf.1      _ = ↑C₁ ^ p₁.toReal * eLpNorm f p μ ^ p.toReal * (d ^ p₁.toReal)⁻¹ * (t ^ p₁.toReal) := by        rw [ha, ← ENNReal.rpow_mul, div_mul_cancel₀]        · rw [ENNReal.div_rpow_of_nonneg, div_eq_mul_inv] <;> try positivity          ring        · exact (sub_pos.mpr (toReal_strict_mono hp₁.ne_top hp₁p)).ne'      _ = _ := by        nth_rw 2 [← one_mul (t ^ p₁.toReal)]        congr        rw [hdeq, ENNReal.rpow_inv_rpow hp₁'  _, ENNReal.mul_inv_cancel term_pos.ne' (by finiteness)]  apply nonpos_iff_eq_zero.mp  calc  _ ≤ distribution (T' (trunc f a)) (eLpNormEssSup (T' (trunc f a)) ν) ν := by gcongr  _ = _ := meas_eLpNormEssSup_lt