De Giorgi preiter on concentric Balls of ball Pos Part

theorem deGiorgi_preiter_on_concentricBalls_of_ballPosPart    {u η : E → ℝ} {x₀ : E} {r s θ lam Cη : ℝ}    (hd : 2 < (d : ℝ))    (A : EllipticCoeff d (Metric.ball x₀ s))    (hr : 0 < r) (hrs : r < s)    (hsub : IsSubsolution A u)    (hu : MemW1pWitness 2 u (Metric.ball x₀ s))    (hwθ : MemW1pWitness 2 (positivePartSub u θ) (Metric.ball x₀ s))    (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  have hs : 0 < s := lt_trans hr hrs  have hd_pos : 0 < (d : ℝ) := by    linarith  have hRatio_nonneg : 0 ≤ ellipticityRatio A := A.ellipticityRatio_nonneg  have hCenergy_nonneg : 0 ≤ 8 * (ellipticityRatio A + 1) * Cη ^ 2 := by    have hCη_sq_nonneg : 0 ≤ Cη ^ 2 := sq_nonneg Cη    nlinarith  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  obtain ⟨hwηθ, hsob⟩ :=    deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart      (d := d) hd hr hrs hu hwθ hθl hη hη_nonneg hη_eq_one hη_bound hη_sub_ball  let hwφ : MemW1pWitness 2 (deGiorgiCutoffTestGeneral η u θ) (Metric.ball x₀ s) :=    deGiorgiCutoffTestWitnessWeighted      isOpen_ball hwθ hη (by norm_num) hCη hη_bound hη_grad_bound  have hweighted :      ∫ x in Metric.ball x₀ s, η x ^ 2 * ‖hwθ.weakGrad x‖ ^ 2 ∂volume ≤        (4 * ellipticityRatio A) *          ∫ x in Metric.ball x₀ s, ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u θ x| ^ 2            ∂volume := by    simpa [mul_assoc, mul_left_comm, mul_comm] using      caccioppoli_weighted_on_ball_of_ballPosPart        A hs hsub hu hwθ hη hη_nonneg hη_bound hCη hη_grad_bound hη_sub_ball  have hgrad_bound_phi :      ∫ x in Metric.ball x₀ s, ‖hwφ.weakGrad x‖ ^ 2 ∂volume ≤        (8 * (ellipticityRatio A + 1) * Cη ^ 2) *          ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume := by    simpa [hwφ] using      deGiorgi_cutoff_gradient_bound_of_weighted        (x₀ := x₀) (s := s) (u := u) (η := η) (k := θ)        (Cη := Cη) (Cw := ellipticityRatio A)        hRatio_nonneg hwθ hη hη_nonneg hη_bound hCη hη_grad_bound hweighted  have hgrad_ae :      hwηθ.weakGrad =ᵐ[volume.restrict (Metric.ball x₀ s)] hwφ.weakGrad :=    MemW1pWitness.ae_eq isOpen_ball hwηθ hwφ  have hgrad_eq :      ∫ x in Metric.ball x₀ s, ‖hwηθ.weakGrad x‖ ^ 2 ∂volume =        ∫ x in Metric.ball x₀ s, ‖hwφ.weakGrad x‖ ^ 2 ∂volume := by    refine integral_congr_ae ?_    filter_upwards [hgrad_ae] with x hx    simp [hx]  have henergy :      ∫ x in Metric.ball x₀ s, ‖hwηθ.weakGrad x‖ ^ 2 ∂volume ≤        (8 * (ellipticityRatio A + 1) * Cη ^ 2) *          ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume := by    rw [hgrad_eq]    exact hgrad_bound_phi  haveI : IsFiniteMeasure (volume.restrict (Metric.ball x₀ s)) := by    rw [isFiniteMeasure_restrict]    exact measure_ball_lt_top.ne  simpa [mul_assoc, mul_left_comm, mul_comm] using    deGiorgi_preiter_of_energy      (μ := volume.restrict (Metric.ball x₀ s))      (d := d) hd_pos (u := u) (θ := θ) (lam := lam)      (Ilam := ∫ x in Metric.ball x₀ r, |positivePartSub u lam x| ^ 2 ∂volume)      (Iθ := ∫ x in Metric.ball x₀ s, |positivePartSub u θ x| ^ 2 ∂volume)      (G := ∫ x in Metric.ball x₀ s, ‖hwηθ.weakGrad x‖ ^ 2 ∂volume)      (Csob := (C_gns d 2) ^ 2)      (Cenergy := 8 * (ellipticityRatio A + 1) * Cη ^ 2)      hθl      (sq_nonneg _)      hCenergy_nonneg      hIθ_nonneg      hθ_int      hsob      henergy      (by rfl)