De Giorgi preiter on concentric Balls of pos Part Approx

theorem deGiorgi_preiter_on_concentricBalls_of_posPartApprox    {u η : E → ℝ} {x₀ : E} {r s θ lam Cη : ℝ}    (hd : 2 < (d : ℝ))    (A : EllipticCoeff d (Metric.ball x₀ s))    (hs : 0 < s) (hr : 0 < r) (hrs : r < s)    (hsub : IsSubsolution A u)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (happroxBallTheta :      ∃ ψ : ℕ → E → ℝ,        (∀ n, ContDiff ℝ 1 (ψ n)) ∧        (∀ n, HasCompactSupport (ψ n)) ∧        Tendsto          (fun n =>            eLpNorm (fun x => ψ n x - (u x - θ)) 2              (volume.restrict (Metric.ball x₀ s)))          atTop (nhds 0) ∧        (∀ i : Fin d,          Tendsto            (fun n =>              eLpNorm                (fun x =>                  (fderiv ℝ (ψ n) x) (EuclideanSpace.single i 1) - hu.weakGrad x i)                2 (volume.restrict (Metric.ball x₀ s)))            atTop (nhds 0)))    (hθl : θ < lam)    (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) :    ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume ≤      (C_gns d 2) ^ 2 * (8 * (ellipticityRatio A + 1) * 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  let hwθ : MemW1pWitness 2 (positivePartSub u θ) (Metric.ball x₀ s) :=    positivePartSub_memW1pWitness_on_ball hs hu θ happroxBallTheta  change    ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume ≤      (C_gns d 2) ^ 2 * (8 * (ellipticityRatio A + 1) * 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  exact    deGiorgi_preiter_on_concentricBalls_of_ballPosPart      (d := d) hd A hr hrs hsub hu hwθ hθl hη hη_nonneg hη_eq_one hη_bound      hCη hη_grad_bound hη_sub_ball