De Giorgi preiter of ball Sobolev on concentric Balls of ball Pos Part

theorem deGiorgi_preiter_of_ballSobolev_on_concentricBalls_of_ballPosPart    {u η : E → ℝ} {x₀ : E} {r s θ lam Csob Cη : ℝ}    (hd : 0 < (d : ℝ))    (A : EllipticCoeff d (Metric.ball x₀ s))    (hr : 0 < r) (hrs : r < s)    (hθl : θ < lam)    (hCsob : 0 ≤ Csob)    (hsub : IsSubsolution A u)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (hwθ : MemW1pWitness 2 (positivePartSub u θ) (Metric.ball x₀ s))    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hη_nonneg : ∀ x, 0 ≤ η x)    (hη_eq_one : ∀ x ∈ Metric.ball x₀ r, η x = 1)    (hη_bound : ∀ x, |η x| ≤ 1)    (hCη : 0 ≤ Cη)    (hη_grad_bound : ∀ x, ‖fderiv ℝ η x‖ ≤ Cη)    (hη_sub_ball : tsupport η ⊆ Metric.ball x₀ s)    (hsob :      ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume ≤        Csob * (∫ x in Metric.ball x₀ r, ‖hwθ.weakGrad x‖ ^ 2 ∂volume) *          ((volume.restrict (Metric.ball x₀ s)).real {x | lam < u x}) ^ (2 / (d : ℝ))) :    ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume ≤      Csob * (4 * ellipticityRatio A * Cη ^ 2) *        ((((lam - θ) ^ 2)⁻¹ *            ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume) ^ (2 / (d : ℝ))) *          ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume := by  haveI : IsFiniteMeasure (volume.restrict (Metric.ball x₀ s)) := by    rw [isFiniteMeasure_restrict]    exact measure_ball_lt_top.ne  have hθ_int :      Integrable (fun x => |positivePartSub u θ x| ^ 2)        (volume.restrict (Metric.ball x₀ s)) := by    simpa [pow_two] using hwθ.memLp.integrable_sq  have hIθ_nonneg :      0 ≤ ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume := by    refine integral_nonneg ?_    intro x    positivity  have henergy :      ∫ x in Metric.ball x₀ r, ‖hwθ.weakGrad x‖ ^ 2 ∂volume ≤        (4 * ellipticityRatio A * Cη ^ 2) *          ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume := by    simpa using      deGiorgi_energy_estimate_on_concentricBalls_of_ballPosPart        A hr hrs hsub hu hwθ hη hη_nonneg hη_eq_one hη_bound hCη        hη_grad_bound hη_sub_ball  exact    deGiorgi_preiter_of_energy      (μ := volume.restrict (Metric.ball x₀ s))      hd hθl hCsob      (by        have hRatio_nonneg : 0 ≤ ellipticityRatio A := A.ellipticityRatio_nonneg        have hCη_sq_nonneg : 0 ≤ Cη ^ 2 := sq_nonneg Cη        nlinarith)      hIθ_nonneg hθ_int      hsob henergy      (by rfl)