Linfty subsolution Moser on ball

theorem linfty_subsolution_Moser_on_ball    (hd : 2 < (d : ℝ))    {x₀ : E} {R : ℝ} (hR : 0 < R)    (A : NormalizedEllipticCoeff d (Metric.ball x₀ R))    {u : E → ℝ} {p₀ : ℝ} (hp₀ : 1 < p₀)    (hsub : IsSubsolution A.1 u)    (hposInt :      IntegrableOn (fun x => |max (u x) 0| ^ p₀) (Metric.ball x₀ R) volume) :    ∀ᵐ x ∂(volume.restrict (Metric.ball x₀ (R / 2 : ℝ))),      |max (u x) 0| ^ p₀ ≤        C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *          (p₀ / (p₀ - 1)) ^ (d : ℝ) *          ((R ^ Module.finrank ℝ E)⁻¹ *            ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume) := by  let uR : E → ℝ := rescaleToUnitBall (d := d) (x₀ := x₀) (R := R) u  let AR : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1) :=    rescaleNormalizedCoeffToUnitBall (d := d) (x₀ := x₀) (R := R) hR A  have hsubR : IsSubsolution AR.1 uR := by    change IsSubsolution      (rescaleCoeffToUnitBall (d := d) (x₀ := x₀) (R := R) hR A.1)      (rescaleToUnitBall (d := d) (x₀ := x₀) (R := R) u)    exact rescaleToUnitBall_isSubsolution (d := d) (x₀ := x₀) (R := R) hR A.1 hsub  have hIntR :      IntegrableOn (fun z => |max (uR z) 0| ^ p₀) (Metric.ball (0 : E) 1) volume := by    dsimp [uR]    have hposInt' :        IntegrableOn (fun x => |max (u x) 0| ^ p₀) (Metric.ball x₀ (R * (1 : ℝ))) volume := by      simpa using hposInt    exact (integrableOn_rescaleToUnitBall_iff      (d := d) (x₀ := x₀) (R := R) (ρ := (1 : ℝ)) hR      (f := fun x => |max (u x) 0| ^ p₀)).2 hposInt'  have hInt_eq :      ∫ z in Metric.ball (0 : E) 1, |max (uR z) 0| ^ p₀ ∂volume =        (R ^ Module.finrank ℝ E)⁻¹ *          ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume := by    simpa [uR] using integral_comp_affine_ball      (d := d) (x₀ := x₀) (R := R) (ρ := (1 : ℝ)) hR      (fun x => |max (u x) 0| ^ p₀)  have hunit :      ∀ᵐ z ∂(volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))),        |max (u (x₀ + R • z)) 0| ^ p₀ ≤          C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *            (p₀ / (p₀ - 1)) ^ (d : ℝ) *            ((R ^ Module.finrank ℝ E)⁻¹ *              ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume) := by    have hbase := linfty_subsolution_Moser (d := d) hd AR hp₀ hsubR hIntR    rw [hInt_eq] at hbase    simpa [uR, AR] using hbase  have hRhalf : R * (1 / 2 : ℝ) = R / 2 := by    ring  have hmap_half :      Measure.map (fun x : E => R⁻¹ • (x - x₀))        (volume.restrict (Metric.ball x₀ (R / 2 : ℝ))) =      ENNReal.ofReal (|R⁻¹ ^ Module.finrank ℝ E|⁻¹) •        (volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))) := by    simpa [hRhalf] using      inverse_affine_map_restrict_ball_mul        (d := d) (x₀ := x₀) (R := R) (ρ := (1 / 2 : ℝ)) hR  have hscaled :      ∀ᵐ z ∂ ENNReal.ofReal (|R⁻¹ ^ Module.finrank ℝ E|⁻¹) •          (volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))),        |max (u (x₀ + R • z)) 0| ^ p₀ ≤          C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *            (p₀ / (p₀ - 1)) ^ (d : ℝ) *            ((R ^ Module.finrank ℝ E)⁻¹ *              ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume) := by    rw [ae_iff]    rw [Measure.smul_apply]    rw [ae_iff] at hunit    rw [hunit]    simp  have hmap_event :      ∀ᵐ z ∂ Measure.map (fun x : E => R⁻¹ • (x - x₀))          (volume.restrict (Metric.ball x₀ (R / 2 : ℝ))),        |max (u (x₀ + R • z)) 0| ^ p₀ ≤          C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *            (p₀ / (p₀ - 1)) ^ (d : ℝ) *            ((R ^ Module.finrank ℝ E)⁻¹ *              ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume) := by    rw [hmap_half]    exact hscaled  have htarget :      ∀ᵐ x ∂(volume.restrict (Metric.ball x₀ (R / 2 : ℝ))),        |max (u (x₀ + R • (R⁻¹ • (x - x₀)))) 0| ^ p₀ ≤          C_Moser d * A.1.Λ ^ ((d : ℝ) / 2) *            (p₀ / (p₀ - 1)) ^ (d : ℝ) *            ((R ^ Module.finrank ℝ E)⁻¹ *              ∫ x in Metric.ball x₀ R, |max (u x) 0| ^ p₀ ∂volume) := by    exact ae_of_ae_map      (((measurable_const_smul R⁻¹).comp (measurable_id.sub measurable_const)).aemeasurable)      hmap_event  filter_upwards [htarget] with x hx  have hcancel : x₀ + R • (R⁻¹ • (x - x₀)) = x := by    calc      x₀ + R • (R⁻¹ • (x - x₀)) = x₀ + (R * R⁻¹) • (x - x₀) := by        rw [smul_smul]      _ = x₀ + (1 : ℝ) • (x - x₀) := by        simp [hR.ne']      _ = x := by        simp  simpa [hcancel] using hx