Linfty subsolution De Giorgi ae of unit Ball height bound

theorem linfty_subsolution_DeGiorgi_ae_of_unitBall_height_bound    {u : E → ℝ} {x₀ : E} {K lamStar : ℝ}    (hd : 2 < (d : ℝ))    (hK : 0 < K) (hLamStar : 0 < lamStar)    (hposInt :      IntegrableOn (fun x => |max (u x) 0| ^ 2)        (Metric.ball x₀ 1) volume)    (hStarInt :      IntegrableOn (fun x => |positivePartSub u lamStar x| ^ 2)        (Metric.ball x₀ (1 / 2 : ℝ)) volume)    (hAint :      ∀ n,        IntegrableOn (fun x => |positivePartSub u (deGiorgiLevel lamStar n) x| ^ 2)          (Metric.ball x₀ (deGiorgiRadius n)) volume)    (hpre :      ∀ n,        deGiorgiEnergySeq u x₀ lamStar (n + 1) ≤          K / ((deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 *            (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ))) *          deGiorgiEnergySeq u x₀ lamStar n ^ (1 + 2 / (d : ℝ)))    (hheight :      C_DeGiorgiSmallness d K *        Real.sqrt (∫ x in Metric.ball x₀ 1, |max (u x) 0| ^ 2 ∂volume) ≤          lamStar) :    ∀ᵐ x ∂(volume.restrict (Metric.ball x₀ (1 / 2 : ℝ))),      max (u x) 0 ≤ lamStar := by  have hI₀_nonneg :      0 ≤ ∫ x in Metric.ball x₀ 1, |max (u x) 0| ^ 2 ∂volume := by    refine integral_nonneg ?_    intro x    positivity  have hsmall0 :      ∫ x in Metric.ball x₀ 1, |max (u x) 0| ^ 2 ∂volume ≤        (deGiorgiRecurrenceCoeff d K lamStar) ^ (-(1 : ℝ) / (2 / (d : ℝ))) *          (deGiorgiRecurrenceBase d) ^ (-(1 : ℝ) / (2 / (d : ℝ)) ^ 2) :=    deGiorgi_initial_energy_small_of_height_bound hK hLamStar hI₀_nonneg hheight  exact linfty_subsolution_DeGiorgi_ae_of_unitBall_initial_energy_smallness    hd hK hLamStar hposInt hStarInt hAint hpre hsmall0