MeasureTheory.weaktype_estimate

lemma weaktype_estimate {C₀ : ℝ≥0} {p : ℝ≥0∞} {q : ℝ≥0∞} {f : α → ε₁}      (hq : 0 < q) (hq' : q < ⊤) (hf : MemLp f p μ)    (h₀T : HasWeakType T p q μ ν C₀) (ht : 0 < t) :    distribution (T f) t ν ≤ C₀ ^ q.toReal *        eLpNorm f p μ ^ q.toReal * (t ^ (-q.toReal)) := by  by_cases ht' : t = ⊤  · simp [ht']  have wt_est := (h₀T f hf).2 -- the weaktype estimate  have q_pos : 0 < q.toReal := toReal_pos hq.ne' hq'.ne_top  have tq_pos : 0 < t ^ q.toReal := ENNReal.rpow_pos_of_nonneg ht q_pos.le  simp only [wnorm, wnorm', hq'.ne_top, ↓reduceIte, iSup_le_iff] at wt_est  have wt_est_t := wt_est t.toNNReal -- this is the weaktype estimate applied to t  have : ofNNReal t.toNNReal = t := coe_toNNReal ht'  rw [this, mul_le_iff_le_inv ht.ne' ht', mul_comm, ENNReal.rpow_inv_le_iff q_pos,      ENNReal.mul_rpow_of_nonneg _ _ q_pos.le, ENNReal.mul_rpow_of_nonneg _ _ q_pos.le,      ← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul, neg_one_mul] at wt_est_t; exact wt_est_t