Linfty subsolution De Giorgi

theorem linfty_subsolution_DeGiorgi    (hd : 2 < (d : ℝ))    (A : EllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ}    (hsub : IsSubsolution A 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 ≤        C_DeGiorgi_subsolution d A *          Real.sqrt (∫ 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  have hI₀_nonneg : 0 ≤ I₀ := by    dsimp [I₀]    refine integral_nonneg ?_    intro x    positivity  obtain ⟨hK, hiter⟩ :=    deGiorgi_iteration_package_on_unitBall_of_subsolution (d := d) hd A hsub  by_cases hI₀_zero : I₀ = 0  · have hposInt_half :        IntegrableOn (fun x => |max (u x) 0| ^ 2)          (Metric.ball (0 : E) (1 / 2 : ℝ)) volume :=      hposInt.mono_set (Metric.ball_subset_ball (by norm_num : (1 / 2 : ℝ) ≤ 1))    have hnonneg : ∀ x, 0 ≤ |max (u x) 0| ^ 2 := by      intro x      positivity    have hbound_half :        ∀ n : ℕ,          ∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |max (u x) 0| ^ 2 ∂volume ≤ (0 : ℝ) := by      intro n      calc        ∫ x in Metric.ball (0 : E) (1 / 2 : ℝ), |max (u x) 0| ^ 2 ∂volume            ≤ ∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume := by                exact setIntegral_mono_set hposInt (ae_of_all _ hnonneg)                  (ae_of_all _ (Metric.ball_subset_ball (by norm_num : (1 / 2 : ℝ) ≤ 1)))        _ = 0 := by              simpa [I₀] using hI₀_zero    have hzero_ae :        ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))), max (u x) 0 = 0 := by      refine ae_eq_zero_of_forall_setIntegral_sq_le_of_tendsto_zero hposInt_half hbound_half ?_      exact (tendsto_const_nhds : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (nhds 0))    filter_upwards [hzero_ae] with x hx    have hrhs_zero :        C_DeGiorgi_subsolution d A * Real.sqrt I₀ = 0 := by      simp [I₀, hI₀_zero]    rw [hrhs_zero]    simp [hx]  · have hI₀_pos : 0 < I₀ := lt_of_le_of_ne hI₀_nonneg (by simpa [eq_comm] using hI₀_zero)    let lamStar : ℝ := C_DeGiorgi_subsolution d A * Real.sqrt I₀    have hLamStar : 0 < lamStar := by      dsimp [lamStar, I₀]      exact deGiorgi_exact_height_threshold_on_unitBall        (d := d) (K := K_DeGiorgi_subsolution d A) hK hI₀_pos    obtain ⟨hStarInt, htail⟩ := hiter hLamStar    obtain ⟨hAint, hpre⟩ := htail    simpa [lamStar, I₀] using      (linfty_subsolution_DeGiorgi_ae_of_unitBall_height_bound        (d := d) (u := u) (x₀ := (0 : E)) (K := K_DeGiorgi_subsolution d A)        (lamStar := lamStar) hd hK hLamStar hposInt hStarInt hAint hpre        (by simp [lamStar, I₀, C_DeGiorgi_subsolution]))