Linfty subsolution De Giorgi exists threshold

theorem linfty_subsolution_DeGiorgi_exists_threshold    (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) :    ∃ lamStar : ℝ,      0 < lamStar ∧      C_DeGiorgi_subsolution d A *        Real.sqrt (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) ≤          lamStar ∧      ∀ᵐ x ∂(volume.restrict (Metric.ball (0 : E) (1 / 2 : ℝ))),        max (u x) 0 ≤ lamStar := 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  have hbound := linfty_subsolution_DeGiorgi (d := d) hd A hsub hposInt  by_cases hI₀_zero : I₀ = 0  · refine ⟨1, by norm_num, ?_, ?_⟩    · have hsmall_zero :          C_DeGiorgi_subsolution d A * Real.sqrt I₀ = 0 := by        simp [I₀, hI₀_zero]      rw [hsmall_zero]      norm_num    · filter_upwards [hbound] with x hx      have hsqrt_zero :          Real.sqrt (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) = 0 := by        rw [show (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) = I₀ by rfl, hI₀_zero]        simp      have hsmall_zero' :          C_DeGiorgi_subsolution d A *              Real.sqrt (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) = 0 := by        rw [hsqrt_zero]        ring      have hx_pair :          u x ≤              C_DeGiorgi_subsolution d A *                Real.sqrt (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) ∧            0 ≤              C_DeGiorgi_subsolution d A *                Real.sqrt (∫ x in Metric.ball (0 : E) 1, |max (u x) 0| ^ 2 ∂volume) := by        simpa using hx      rw [hsmall_zero'] at hx_pair      have hx_zero : max (u x) 0 ≤ 0 := by        exact max_le_iff.mpr ⟨hx_pair.1, le_rfl⟩      linarith  · let lamStar : ℝ := C_DeGiorgi_subsolution d A * Real.sqrt I₀    have hLamStar : 0 < lamStar := by      have hI₀_pos : 0 < I₀ := lt_of_le_of_ne hI₀_nonneg (by simpa [eq_comm] using hI₀_zero)      dsimp [lamStar, I₀]      exact deGiorgi_exact_height_threshold_on_unitBall        (d := d) (K := K_DeGiorgi_subsolution d A)        (K_DeGiorgi_subsolution_pos (d := d) A) hI₀_pos    refine ⟨lamStar, hLamStar, le_rfl, ?_⟩    simpa [lamStar, I₀] using hbound