Supersolution ae closeout inv

theorem supersolution_ae_closeout_inv    (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)    (hpInt :      IntegrableOn (fun x => |(u x)⁻¹| ^ p₀)        (Metric.ball (0 : E) 1) volume) :    ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))),      |(u x)⁻¹| ^ p₀ ≤        C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *          ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume := by  let Bhalf : Set E := Metric.ball (0 : E) (1 / 2 : ℝ)  let μ : Measure E := volume.restrict Bhalf  let f : E → ℝ := fun x => |(u x)⁻¹|  let g : E → ℝ := fun x => f x ^ (p₀ / 2)  let K : ℝ :=    (C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *      ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume) ^ (1 / 2 : ℝ)  haveI : IsFiniteMeasure μ := by    dsimp [μ, Bhalf]    rw [isFiniteMeasure_restrict]    exact measure_ne_top_of_subset Metric.ball_subset_closedBall      (isCompact_closedBall (0 : E) (1 / 2 : ℝ)).measure_lt_top.ne  have hK_nonneg : 0 ≤ K := by    dsimp [K]    exact Real.rpow_nonneg (supersolutionInvBoundPow_nonneg (d := d) A) _  have hiter :      ∀ n,        IntegrableOn (fun x => |(u x)⁻¹| ^ moserExponentSeq d p₀ n)          (Metric.ball (0 : E) (moserRadius n)) volume ∧        superIterNormInv (d := d) (u := u) p₀ n ≤          ((C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *            superIterNormInv (d := d) (u := u) p₀ 0 := by    intro n    have hraw := supersolution_iteration_inverse (d := d) hd A hp₀ hu_pos hsuper hpInt n    have hgeom := supersolution_geometric_majorant_inv (d := d) hd A hp₀ n    refine ⟨hraw.1, ?_⟩    calc      superIterNormInv (d := d) (u := u) p₀ n          ≤ (∏ i ∈ Finset.range n, superStepConstInv (d := d) A p₀ i) *              superIterNormInv (d := d) (u := u) p₀ 0 := hraw.2      _ ≤ ((C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2)) ^            (1 / p₀)) *            superIterNormInv (d := d) (u := u) p₀ 0 := by            exact mul_le_mul_of_nonneg_right hgeom              (by                dsimp [superIterNormInv]                exact Real.rpow_nonneg (integral_nonneg fun x => by positivity) _)  have hbound_all :      ∀ m : ℕ, ∀ᵐ x ∂μ, g x < K + 1 / (m + 1 : ℝ) := by    intro m    have hzero :        μ.real {x | K + 1 / (m + 1 : ℝ) ≤ g x} = 0 := by      refine supersolution_closeout_superlevel_null (d := d) hd A (u := u) hp₀ hiter ?_      dsimp [K]      have hfrac_pos : 0 < 1 / (m + 1 : ℝ) := by positivity      linarith    rw [ae_iff]    simpa [μ, Bhalf, g, K, not_lt] using      (measureReal_eq_zero_iff        (μ := μ) (s := {x | K + 1 / (m + 1 : ℝ) ≤ g x})        (measure_ne_top μ {x | K + 1 / (m + 1 : ℝ) ≤ g x})).1 hzero  have hbound_ae :      ∀ᵐ x ∂μ, ∀ m : ℕ, g x < K + 1 / (m + 1 : ℝ) := by    exact ae_all_iff.2 hbound_all  filter_upwards [hbound_ae] with x hx  have hfx_nonneg : 0 ≤ f x := by    dsimp [f]    exact abs_nonneg ((u x)⁻¹)  have hgx_nonneg : 0 ≤ g x := by    dsimp [g]    exact Real.rpow_nonneg hfx_nonneg _  have hgx_le : g x ≤ K := by    by_contra hgx_gt    have hgap_pos : 0 < g x - K := by linarith    obtain ⟨m, hm⟩ := exists_nat_one_div_lt hgap_pos    have hlt : K + 1 / (m + 1 : ℝ) < g x := by linarith    linarith [hx m]  have hgpow :      g x ^ (2 : ℝ) ≤ K ^ (2 : ℝ) := by    exact Real.rpow_le_rpow hgx_nonneg hgx_le (by norm_num)  have hg_sq_eq : g x ^ (2 : ℝ) = f x ^ p₀ := by    calc      g x ^ (2 : ℝ) = (f x ^ (p₀ / 2)) ^ (2 : ℝ) := by rfl      _ = f x ^ ((p₀ / 2) * 2) := by rw [← Real.rpow_mul hfx_nonneg]      _ = f x ^ p₀ := by            congr 2            ring  have hK_sq_eq :      K ^ (2 : ℝ) =        C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *          ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume := by    calc      K ^ (2 : ℝ)          =            (C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *              ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume) ^              ((1 / 2 : ℝ) * 2) := by                dsimp [K]                rw [← Real.rpow_mul (supersolutionInvBoundPow_nonneg (d := d) A)]      _ =            C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *              ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume := by                rw [show ((1 / 2 : ℝ) * 2) = (1 : ℝ) by ring, Real.rpow_one]  calc    |(u x)⁻¹| ^ p₀ = f x ^ p₀ := by rfl    _ = g x ^ (2 : ℝ) := hg_sq_eq.symm    _ ≤ K ^ (2 : ℝ) := hgpow    _ = C_weakHarnack0 d * (A.1.Λ * p₀ ^ 2 + 1) ^ ((d : ℝ) / 2) *          ∫ x in Metric.ball (0 : E) 1, |(u x)⁻¹| ^ p₀ ∂volume := hK_sq_eq