Weak harnack stage one forward

theorem weak_harnack_stage_one_forward    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ} {p q : ℝ}    (hp : 0 < p) (hp1 : p < 1) (hpq : p < q) (hq1 : q < 1)    (hu_pos : ∀ x ∈ Metric.ball (0 : E) 1, 0 < u x)    (hsuper : IsSupersolution A.1 u) :    (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ),        |u x| ^ (q * (d : ℝ) / ((d : ℝ) - 2)) ∂volume) ^          (p * (((d : ℝ) - 2) / (q * (d : ℝ)))) ≤      C_weakHarnack0Forward (d := d) hd *        (A.1.Λ * p ^ 2 / (1 - q) ^ 2 + 1) ^ (((d : ℝ) * moserChi d) / 2) *        ∫ x in Metric.ball (0 : E) 1, |u x| ^ p ∂volume := by  have hq : 0 < q := lt_trans hp hpq  let qχ : ℝ := q * moserChi d  have hqχ_pos : 0 < qχ := mul_pos hq (moserChi_pos (d := d) hd)  have hqχ_ne : qχ ≠ 0 := hqχ_pos.ne'  rcases exists_forward_iteration_depth (d := d) hd hp hpq with    ⟨m, hm_lt, hm_le⟩  let p₀ : ℝ := q * (moserChi d)⁻¹ ^ m  have hp₀ : 0 < p₀ := by    dsimp [p₀]    exact mul_pos hq (pow_pos (inv_pos.mpr (moserChi_pos (d := d) hd)) m)  have hp₀_lt_p : p₀ < p := by    simpa [p₀] using hm_lt  have hp_le_chi_p₀ : p ≤ moserChi d * p₀ := by    simpa [p₀] using hm_le  have hp₀_le_two : p₀ ≤ 2 := by    have hp₀_lt_one : p₀ < 1 := lt_trans hp₀_lt_p hp1    linarith  have hp₀Int :      IntegrableOn (fun x => |u x| ^ p₀)        (Metric.ball (0 : E) 1) volume := by    exact supersolution_integrableOn_ball_one_rpow      (d := d) A hp₀ hp₀_le_two hsuper  have hiter :=    supersolution_iteration_forward (d := d) hd A (u := u) (q := q) (m := m)      hq hq1 hu_pos hsuper  have hstep := hiter hp₀Int (m + 1) le_rfl  have hgeom :=    supersolution_geometric_majorant_fwd (d := d) hd A (q := q) (m := m) hq hq1  have htarget_int :      IntegrableOn (fun x => |u x| ^ qχ)        (Metric.ball (0 : E) (moserRadius (m + 1))) volume := by    have hstep_int := hstep.1    rw [moserExponentSeq_forward_target_eq (d := d) hd (q := q) (m := m)] at hstep_int    simpa [qχ] using hstep_int  have htarget_norm :      (∫ x in Metric.ball (0 : E) (moserRadius (m + 1)),          |u x| ^ qχ ∂volume) ^ (1 / qχ) ≤        ((C_weakHarnack0 d *              (A.1.Λ * p₀ ^ 2 / (1 - q) ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *          (∫ x in Metric.ball (0 : E) 1, |u x| ^ p₀ ∂volume) ^ (1 / p₀) := by    have hbound_step :        superIterNormFwd (d := d) (u := u) p₀ (m + 1) ≤          (∏ i ∈ Finset.range (m + 1), superStepConstFwd (d := d) A p₀ i) *            superIterNormFwd (d := d) (u := u) p₀ 0 := by      simpa [p₀] using hstep.2    calc      (∫ x in Metric.ball (0 : E) (moserRadius (m + 1)),          |u x| ^ qχ ∂volume) ^ (1 / qχ)          = superIterNormFwd (d := d) (u := u) p₀ (m + 1) := by              simpa [qχ, p₀] using                (superIterNormFwd_target (d := d) hd (u := u) (q := q) (m := m)).symm      _ ≤ (∏ i ∈ Finset.range (m + 1), superStepConstFwd (d := d) A p₀ i) *            superIterNormFwd (d := d) (u := u) p₀ 0 := by              exact hbound_step      _ ≤ ((C_weakHarnack0 d *              (A.1.Λ * p₀ ^ 2 / (1 - q) ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *          superIterNormFwd (d := d) (u := u) p₀ 0 := by            exact mul_le_mul_of_nonneg_right (by simpa [p₀] using hgeom)              (Real.rpow_nonneg (integral_nonneg fun x => by positivity) _)      _ = ((C_weakHarnack0 d *              (A.1.Λ * p₀ ^ 2 / (1 - q) ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *          (∫ x in Metric.ball (0 : E) 1, |u x| ^ p₀ ∂volume) ^ (1 / p₀) := by            rw [superIterNormFwd_zero]  have hhalf_sub :      Metric.ball (0 : E) (1 / 2 : ℝ) ⊆ Metric.ball (0 : E) (moserRadius (m + 1)) := by    exact Metric.ball_subset_ball (le_of_lt (moserRadius_gt_half (m + 1)))  have hhalf_int :      IntegrableOn (fun x => |u x| ^ qχ)        (Metric.ball (0 : E) (1 / 2 : ℝ)) volume := by    exact htarget_int.mono_set hhalf_sub  have hhalf_integral_le :      ∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume ≤        ∫ x in Metric.ball (0 : E) (moserRadius (m + 1)), |u x| ^ qχ ∂volume := by    exact setIntegral_mono_set htarget_int      (ae_of_all _ (by intro x; positivity))      (Filter.Eventually.of_forall hhalf_sub)  have hhalf_norm_le :      (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume) ^ (1 / qχ) ≤        ((C_weakHarnack0 d *              (A.1.Λ * p₀ ^ 2 / (1 - q) ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *          (∫ x in Metric.ball (0 : E) 1, |u x| ^ p₀ ∂volume) ^ (1 / p₀) := by    exact      (Real.rpow_le_rpow (by positivity) hhalf_integral_le (by positivity)).trans        htarget_norm  have hmain_pow :      (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume) ^ (p / qχ) ≤        weakHarnackForwardUpgradeLHS (d := d) A u p q p₀ := by    calc      (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume) ^ (p / qχ)          = ((∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume) ^              (1 / qχ)) ^ p := by                rw [← Real.rpow_mul (integral_nonneg fun x => by positivity)]                field_simp [hqχ_ne]      _ ≤ weakHarnackForwardUpgradeLHS (d := d) A u p q p₀ := by            exact Real.rpow_le_rpow (by positivity) hhalf_norm_le hp.le  have hupgrade :=    weak_harnack_stage_one_forward_power_upgrade      (d := d) hd A (u := u) hp₀ hp hp1 hp₀_lt_p hp_le_chi_p₀ hq1 hsuper hp₀Int  have hqχ_eq : q * (d : ℝ) / ((d : ℝ) - 2) = qχ := by    dsimp [qχ]    rw [moserChi]    ring  have hexp_eq : p * (((d : ℝ) - 2) / (q * (d : ℝ))) = p / qχ := by    dsimp [qχ]    rw [moserChi]    field_simp [hq.ne']  calc    (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ),        |u x| ^ (q * (d : ℝ) / ((d : ℝ) - 2)) ∂volume) ^          (p * (((d : ℝ) - 2) / (q * (d : ℝ))))        = (∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |u x| ^ qχ ∂volume) ^            (p / qχ) := by              rw [hqχ_eq, hexp_eq]    _ ≤ weakHarnackForwardUpgradeLHS (d := d) A u p q p₀ := hmain_pow    _ ≤ weakHarnackForwardUpgradeRHS (d := d) hd A u p q := hupgrade    _ = C_weakHarnack0Forward (d := d) hd *          (A.1.Λ * p ^ 2 / (1 - q) ^ 2 + 1) ^ (((d : ℝ) * moserChi d) / 2) *          ∫ x in Metric.ball (0 : E) 1, |u x| ^ p ∂volume := rfl