Weak harnack stage one inverse

theorem weak_harnack_stage_one_inverse    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ} {p₀ : ℝ} (hp₀ : 0 < p₀)    (hu_pos : ∀ x ∈ Metric.ball (0 : E) 1, 0 < u x)    (hsuper : IsSupersolution A.1 u) :    (A.1.Λ * p₀ ^ 2 + 1) ^ (-(d : ℝ) / 2) *        (∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume)⁻¹ ≤      C_weakHarnack0 d *        (essInf u μhalf) ^ p₀ := by  let I : ℝ := ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume  let L : ℝ := A.1.Λ * p₀ ^ 2 + 1  have hC_nonneg : 0 ≤ C_weakHarnack0 d := by    exact le_trans (by norm_num : (0 : ℝ) ≤ 1) (one_le_C_weakHarnack0 (d := d))  have hL_pos : 0 < L := by    dsimp [L]    nlinarith [A.1.Λ_nonneg, sq_nonneg p₀]  have hL_nonneg : 0 ≤ L := hL_pos.le  have hhalf_nonneg : ∀ᵐ x ∂μhalf, 0 ≤ u x := by    filter_upwards [ae_restrict_mem measurableSet_ball] with x hx    exact (hu_pos x ((Metric.ball_subset_ball (by norm_num : (1 / 2 : ℝ) ≤ 1)) hx)).le  have hessInf_nonneg : 0 ≤ essInf u μhalf := by    exact      le_essInf_real_of_ae_le        (d := d)        (restrict_ball_ne_zero (c := (0 : E)) (r := (1 / 2 : ℝ)) (by norm_num))        hhalf_nonneg  by_cases hpInt : IntegrableOn (fun x => |(u x)⁻¹| ^ p₀) (Metric.ball (0 : E) 1) volume  · let c0 : ℝ := C_weakHarnack0 d * L ^ ((d : ℝ) / 2) * I    have hI_nonneg : 0 ≤ I := by      dsimp [I]      exact integral_nonneg fun x => by positivity    have hI_pos : 0 < I := by      have hnonneg :          0 ≤ᵐ[volume.restrict (Metric.ball (0 : E) 1)] fun x => |(u x)⁻¹| ^ p₀ := by        filter_upwards [ae_restrict_mem measurableSet_ball] with x hx        positivity      have hI_ne_zero : I ≠ 0 := by        intro hI_zero        have hzero_ae :            (fun x => |(u x)⁻¹| ^ p₀) =ᵐ[volume.restrict (Metric.ball (0 : E) 1)] 0 := by          rw [← sub_eq_zero] at hI_zero          rwa [sub_zero, setIntegral_eq_zero_iff_of_nonneg_ae hnonneg hpInt] at hI_zero        have hpos_ae :            ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) 1)), |(u x)⁻¹| ^ p₀ ≠ 0 := by          filter_upwards [ae_restrict_mem measurableSet_ball] with x hx          have hux_pos : 0 < u x := hu_pos x hx          have hpow_pos : 0 < |(u x)⁻¹| ^ p₀ := by            rw [abs_of_pos (inv_pos.mpr hux_pos)]            exact Real.rpow_pos_of_pos (inv_pos.mpr hux_pos) p₀          exact hpow_pos.ne'        have hfalse : ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) 1)), False := by          filter_upwards [hzero_ae, hpos_ae] with x hx0 hxpos          exact hxpos hx0        rw [ae_iff] at hfalse        have hball_zero : volume (Metric.ball (0 : E) 1) = 0 := by          simpa [Measure.restrict_apply_univ] using hfalse        exact (Metric.measure_ball_pos volume (0 : E) (by norm_num : (0 : ℝ) < 1)).ne'          hball_zero      exact lt_of_le_of_ne hI_nonneg (Ne.symm hI_ne_zero)    have hc0_pos : 0 < c0 := by      dsimp [c0]      exact mul_pos (mul_pos (lt_of_lt_of_le zero_lt_one (one_le_C_weakHarnack0 (d := d)))        (Real.rpow_pos_of_pos hL_pos _)) hI_pos    have hc0_nonneg : 0 ≤ c0 := hc0_pos.le    have hclose := supersolution_ae_closeout_inv (d := d) hd A hp₀ hu_pos hsuper hpInt    have hroot_ae :        ∀ᵐ x ∂μhalf, (c0⁻¹) ^ (1 / p₀) ≤ u x := by      filter_upwards [hclose, ae_restrict_mem measurableSet_ball] with x hxclose hxhalf      have hux_pos : 0 < u x := hu_pos x ((Metric.ball_subset_ball (by norm_num : (1 / 2 : ℝ) ≤ 1)) hxhalf)      have hupow_pos : 0 < u x ^ p₀ := Real.rpow_pos_of_pos hux_pos p₀      have hpow_inv : (u x ^ p₀)⁻¹ ≤ c0 := by        calc          (u x ^ p₀)⁻¹ = ((u x)⁻¹) ^ p₀ := by            rw [Real.inv_rpow hux_pos.le]          _ = |(u x)⁻¹| ^ p₀ := by            rw [abs_of_pos (inv_pos.mpr hux_pos)]          _ ≤ c0 := hxclose      have hpow_lower : c0⁻¹ ≤ u x ^ p₀ := by        have htmp :            c0⁻¹ ≤ ((u x ^ p₀)⁻¹)⁻¹ := (inv_le_inv₀ hc0_pos (inv_pos.mpr hupow_pos)).2 hpow_inv        simpa [hupow_pos.ne'] using htmp      have hroot :=        Real.rpow_le_rpow (inv_nonneg.mpr hc0_nonneg) hpow_lower (by positivity : 0 ≤ 1 / p₀)      have hux_root : (u x ^ p₀) ^ (1 / p₀) = u x := by        rw [← Real.rpow_mul hux_pos.le]        field_simp [hp₀.ne']        rw [Real.rpow_one]      calc        (c0⁻¹) ^ (1 / p₀) ≤ (u x ^ p₀) ^ (1 / p₀) := hroot        _ = u x := hux_root    have hc_le_ess : (c0⁻¹) ^ (1 / p₀) ≤ essInf u μhalf := by      exact        le_essInf_real_of_ae_le          (d := d)          (restrict_ball_ne_zero (c := (0 : E)) (r := (1 / 2 : ℝ)) (by norm_num))          hroot_ae    have hpow_ess :        c0⁻¹ ≤ (essInf u μhalf) ^ p₀ := by      have hpow :=        Real.rpow_le_rpow          (Real.rpow_nonneg (inv_nonneg.mpr hc0_nonneg) _)          hc_le_ess hp₀.le      have hleft : ((c0⁻¹) ^ (1 / p₀)) ^ p₀ = c0⁻¹ := by        calc          ((c0⁻¹) ^ (1 / p₀)) ^ p₀ = (c0⁻¹) ^ ((1 / p₀) * p₀) := by            rw [← Real.rpow_mul (inv_nonneg.mpr hc0_nonneg)]          _ = (c0⁻¹) ^ (1 : ℝ) := by            congr 1            field_simp [hp₀.ne']          _ = c0⁻¹ := by rw [Real.rpow_one]      calc        c0⁻¹ = ((c0⁻¹) ^ (1 / p₀)) ^ p₀ := hleft.symm        _ ≤ (essInf u μhalf) ^ p₀ := hpow    have hC_pos : 0 < C_weakHarnack0 d :=      lt_of_lt_of_le zero_lt_one (one_le_C_weakHarnack0 (d := d))    have hLpow_ne : L ^ ((d : ℝ) / 2) ≠ 0 := (Real.rpow_pos_of_pos hL_pos _).ne'    have hLneg : L ^ (-(d : ℝ) / 2) = (L ^ ((d : ℝ) / 2))⁻¹ := by      rw [show (-(d : ℝ) / 2) = -((d : ℝ) / 2) by ring, Real.rpow_neg hL_pos.le]    calc      L ^ (-(d : ℝ) / 2) * I⁻¹          = C_weakHarnack0 d * c0⁻¹ := by              dsimp [c0]              rw [hLneg]              field_simp [hC_pos.ne', hLpow_ne, hI_pos.ne']      _ ≤ C_weakHarnack0 d * (essInf u μhalf) ^ p₀ := by            exact mul_le_mul_of_nonneg_left hpow_ess hC_nonneg  · have hrhs_nonneg : 0 ≤ C_weakHarnack0 d * (essInf u μhalf) ^ p₀ := by      exact mul_nonneg hC_nonneg (Real.rpow_nonneg hessInf_nonneg _)    have hI_zero :        ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume = 0 := by      simpa using (integral_undef hpInt :        ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume = 0)    calc      (A.1.Λ * p₀ ^ 2 + 1) ^ (-(d : ℝ) / 2) *          (∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume)⁻¹          = 0 := by rw [hI_zero]; simp      _ ≤ C_weakHarnack0 d * (essInf u μhalf) ^ p₀ := hrhs_nonneg