MeasureTheory.estimate_norm_rpow_range_operator'

lemma estimate_norm_rpow_range_operator'    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    [TopologicalSpace E₂] [ContinuousENorm E₂]    (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hp₁p : p < p₁) (hp₀p : p₀ < p)    (tc : StrictRangeToneCouple)    (hq₀' : q₀ = ⊤ → ∀ s > 0, distribution (T (truncCompl f (tc.ton s))) s ν = 0)    (hq₁' : q₁ = ⊤ → ∀ s > 0, distribution (T (trunc f (tc.ton s))) s ν = 0)    (hf : MemLp f p μ) (hT₁ : HasWeakType T p₁ q₁ μ ν C₁) (hT₀ : HasWeakType T p₀ q₀ μ ν C₀) :    ∫⁻ s : ℝ≥0∞, distribution (T (trunc f (tc.ton s))) s ν *    s ^ (q.toReal - 1) +    distribution (T (truncCompl f (tc.ton s))) s ν *    s ^ (q.toReal - 1) ≤    (if q₁ < ⊤ then 1 else 0) * (C₁ ^ q₁.toReal * (∫⁻ s : ℝ≥0∞,        eLpNorm (trunc f (tc.ton s)) p₁ μ ^ q₁.toReal *        s ^ (q.toReal - q₁.toReal - 1))) +    (if q₀ < ⊤ then 1 else 0) * (C₀ ^ q₀.toReal * ∫⁻ s : ℝ≥0∞,        eLpNorm (truncCompl f (tc.ton s)) (p₀) μ ^ q₀.toReal *        s ^ (q.toReal - q₀.toReal - 1)) := by  have : ∀ q' q : ℝ, -q' + (q - 1) = q - q' - 1 := by intro q' q; group  repeat rw [← this]  have := hp₁p.le  have := hp₀p.le  have := hp₁p.ne_top  have p_pos : 0 < p := lt_trans hp₀ hp₀p  repeat rw [lintegral_rw₂ (Filter.EventuallyEq.refl _ _) power_aux_3]  nth_rw 2 [← lintegral_const_mul' _ _ (by finiteness)]  nth_rw 1 [← lintegral_const_mul' _ _ (by finiteness)]  simp_rw [← mul_assoc]  split_ifs with is_q₁top is_q₀top  · rw [one_mul, one_mul, ← lintegral_add_left']    · apply lintegral_mono_ae      filter_upwards [ae_in_Ioo_zero_top] with s ⟨s_pos, s_lt_top⟩      gcongr      · have : tc.ton s ≠ ⊤ := (tc.ran_ton s ⟨s_pos, s_lt_top⟩).2.ne        apply weaktype_estimate_trunc p_pos hq₁ _ hp₁p.le <;> assumption      · have : 0 < tc.ton s := (tc.ran_ton s ⟨s_pos, s_lt_top⟩).1        apply weaktype_estimate_truncCompl (p₀ := p₀) hp₀ <;> assumption    · fun_prop  · rw [one_mul, zero_mul, add_zero]    apply lintegral_mono_ae    filter_upwards [ae_in_Ioo_zero_top] with s ⟨s_pos, s_lt_top⟩    have : q₀ = ⊤ := not_lt_top.mp is_q₀top    rw [hq₀' this s s_pos, zero_mul, add_zero]    gcongr    have : tc.ton s ≠ ⊤ := (tc.ran_ton s ⟨s_pos, s_lt_top⟩).2.ne    apply weaktype_estimate_trunc p_pos <;> assumption  · rw [one_mul, zero_mul, zero_add]    apply lintegral_mono_ae    filter_upwards [ae_in_Ioo_zero_top] with s ⟨s_pos, s_lt_top⟩    have : q₁ = ⊤ := not_lt_top.mp is_q₁top    rw [hq₁' this s s_pos, zero_mul, zero_add]    have : 0 < tc.ton s := (tc.ran_ton s ⟨s_pos, s_lt_top⟩).1    gcongr    apply weaktype_estimate_truncCompl (p₀ := p₀) _ hp₁p.ne_top <;> assumption  · simp only [zero_mul, add_zero, nonpos_iff_eq_zero]    have : ∫⁻ _ : ℝ≥0∞, 0 = 0 := lintegral_zero    rw [← this]    apply lintegral_congr_ae    filter_upwards [ae_in_Ioo_zero_top] with s ⟨s_pos, s_lt_top⟩    have is_q₀top : ¬ q₀ < ⊤ := by assumption    rw [hq₀' (not_lt_top.mp is_q₀top) s s_pos, hq₁' (not_lt_top.mp is_q₁top) s s_pos, zero_mul, add_zero]