Linfty subsolution Moser two

theorem linfty_subsolution_Moser_two    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ}    (hsub : IsSubsolution A.1 u)    (hposInt :      IntegrableOn (fun x => |max (u x) 0| ^ 2)        (Metric.ball (0 : E) 1) volume) :    ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))),      |max (u x) 0| ^ 2 ≤        C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *          (2 / (2 - 1 : ℝ)) ^ (d : ℝ) *          ∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume := by  let I₂ : ℝ := ∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume  let c : ℝ := C_DeGiorgi_subsolution_normalized d * A.1.Λ ^ ((d : ℝ) / 4)  have hI₂_nonneg : 0 ≤ I₂ := by    dsimp [I₂]    refine integral_nonneg ?_    intro x    positivity  have hc_nonneg : 0 ≤ c := by    have hCDG_nonneg : 0 ≤ C_DeGiorgi_subsolution_normalized d := by      dsimp [C_DeGiorgi_subsolution_normalized]      exact        (C_DeGiorgiSmallness_pos (d := d)          (K_DeGiorgi_subsolution_normalized_pos (d := d))).le    dsimp [c]    exact mul_nonneg      hCDG_nonneg      (Real.rpow_nonneg A.1.Λ_nonneg _)  filter_upwards    [linfty_subsolution_DeGiorgi_normalized (d := d) hd A hsub hposInt]    with x hx  have hx_nonneg : 0 ≤ max (u x) 0 := by    positivity  have hsq :      |max (u x) 0| ^ 2 ≤ c ^ 2 * I₂ := by    have hx' : max (u x) 0 ≤ c * Real.sqrt I₂ := hx    have hrhs_nonneg : 0 ≤ c * Real.sqrt I₂ := by      exact mul_nonneg hc_nonneg (Real.sqrt_nonneg I₂)    have hsq' : (max (u x) 0) ^ 2 ≤ (c * Real.sqrt I₂) ^ 2 := by      nlinarith    calc      |max (u x) 0| ^ 2 = (max (u x) 0) ^ 2 := by        rw [abs_of_nonneg hx_nonneg]      _ ≤ (c * Real.sqrt I₂) ^ 2 := hsq'      _ = c ^ 2 * I₂ := by        rw [mul_pow, Real.sq_sqrt hI₂_nonneg]  have hconst :      c ^ 2 * I₂ ≤        C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *          (2 / (2 - 1 : ℝ)) ^ (d : ℝ) * I₂ := by    have hbase :        c ^ 2 ≤          C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *            (2 / (2 - 1 : ℝ)) ^ (d : ℝ) := by      have hpow :          (A.1.Λ ^ ((d : ℝ) / 4)) ^ 2 = A.1.Λ ^ ((d : ℝ) / 2) := by        rw [pow_two, ← Real.rpow_add A.1.Λ_pos]        ring_nf      calc        c ^ 2            = (C_DeGiorgi_subsolution_normalized d) ^ 2 *                A.1.Λ ^ ((d : ℝ) / 2) := by                  dsimp [c]                  rw [mul_pow, hpow]        _ ≤ C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) := by            exact mul_le_mul_of_nonneg_right              (C_DeGiorgi_subsolution_normalized_sq_le_C_Moser (d := d))              (Real.rpow_nonneg A.1.Λ_nonneg _)        _ ≤ C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *              (2 / (2 - 1 : ℝ)) ^ (d : ℝ) := by            have hleft_nonneg : 0 ≤ C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) := by              exact mul_nonneg                (le_trans (by norm_num : (0 : ℝ) ≤ 1) (one_le_C_Moser (d := d)))                (Real.rpow_nonneg A.1.Λ_nonneg _)            have hone : (1 : ℝ) ≤ (2 / (2 - 1 : ℝ)) ^ (d : ℝ) := by              have hbase : (1 : ℝ) ≤ 2 / (2 - 1 : ℝ) := by norm_num              have hd_nonneg : 0 ≤ (d : ℝ) := by exact_mod_cast Nat.zero_le d              exact Real.one_le_rpow hbase hd_nonneg            simpa [mul_assoc] using              (mul_le_mul_of_nonneg_left hone hleft_nonneg)    exact mul_le_mul_of_nonneg_right hbase hI₂_nonneg  exact le_trans hsq (by    simpa [I₂] using hconst)