De Giorgi energy estimate on concentric Balls of ball Pos Part

theorem deGiorgi_energy_estimate_on_concentricBalls_of_ballPosPart    {u η : E → ℝ} {x₀ : E} {r s Cη k : ℝ}    (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_trunc : MemW1pWitness 2 (positivePartSub u k) (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) :    ∫ x in Metric.ball x₀ r, ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume ≤      4 * ellipticityRatio A * Cη ^ 2 *        ∫ x in Metric.ball x₀ s, |positivePartSub u k x| ^ 2 ∂volume := by  have hs : 0 < s := lt_trans hr hrs  have htrunc_sq_int :      IntegrableOn (fun x => ‖hw_trunc.weakGrad x‖ ^ 2)        (Metric.ball x₀ s) volume := by    simpa [pow_two] using hw_trunc.weakGrad_norm_memLp.integrable_sq  have hweighted_int :      IntegrableOn (fun x => η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2)        (Metric.ball x₀ s) volume := by    refine Integrable.mono' htrunc_sq_int ?_ ?_    · exact        (((hη.continuous.pow 2).aemeasurable).mul          htrunc_sq_int.aestronglyMeasurable.aemeasurable).aestronglyMeasurable    · filter_upwards with x      have hηx_nonneg : 0 ≤ η x := hη_nonneg x      have hηx_le_one : η x ≤ 1 := by        simpa [abs_of_nonneg hηx_nonneg] using hη_bound x      have hηx_sq_le_one : η x ^ 2 ≤ 1 := by        nlinarith      have hgw_nonneg : 0 ≤ ‖hw_trunc.weakGrad x‖ ^ 2 := by positivity      have hprod_nonneg : 0 ≤ η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 := by positivity      have hle : η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ≤ ‖hw_trunc.weakGrad x‖ ^ 2 := by        nlinarith      simpa [Real.norm_eq_abs, abs_of_nonneg hprod_nonneg, abs_of_nonneg hgw_nonneg] using hle  have hpos_sq_int :      IntegrableOn (fun x => |positivePartSub u k x| ^ 2)        (Metric.ball x₀ s) volume := by    simpa [pow_two] using hw_trunc.memLp.integrable_sq  have hgrad_term_int :      IntegrableOn (fun x => ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2)        (Metric.ball x₀ s) volume := by    refine Integrable.mono' (hpos_sq_int.const_mul (Cη ^ 2)) ?_ ?_    · exact        ((((hη.continuous_fderiv (by simp : ((⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0)).norm.pow 2).aemeasurable).mul          hpos_sq_int.aestronglyMeasurable.aemeasurable).aestronglyMeasurable    · filter_upwards with x      have hfd_sq_le : ‖fderiv ℝ η x‖ ^ 2 ≤ Cη ^ 2 := by        exact sq_le_sq.mpr (by          simpa [abs_of_nonneg (norm_nonneg _), abs_of_nonneg hCη] using hη_grad_bound x)      have hpos_nonneg : 0 ≤ |positivePartSub u k x| ^ 2 := by positivity      have hterm_nonneg :          0 ≤ ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2 := by positivity      have hle :          ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2 ≤            Cη ^ 2 * |positivePartSub u k x| ^ 2 :=        mul_le_mul_of_nonneg_right hfd_sq_le hpos_nonneg      simpa [Real.norm_eq_abs, abs_of_nonneg hterm_nonneg] using hle  have hweighted :      ∫ x in Metric.ball x₀ s, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume ≤        (4 * ellipticityRatio A) *          ∫ x in Metric.ball x₀ s, ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2            ∂volume := by    simpa [mul_assoc, mul_left_comm, mul_comm] using      caccioppoli_weighted_on_ball_of_ballPosPart        A hs hsub hu hw_trunc hη hη_nonneg hη_bound hCη hη_grad_bound hη_sub_ball  have hleft_eq :      ∫ x in Metric.ball x₀ r, ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume =        ∫ x in Metric.ball x₀ r, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume := by    refine integral_congr_ae ?_    refine (ae_restrict_iff' (μ := volume) measurableSet_ball).2 ?_    filter_upwards with x hx    simp [hη_eq_one x hx]  have hweighted_nonneg :      ∀ x, 0 ≤ η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 := by    intro x    positivity  have hleft_mono :      ∫ x in Metric.ball x₀ r, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume ≤        ∫ x in Metric.ball x₀ s, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume := by    exact setIntegral_mono_set hweighted_int      (ae_of_all _ hweighted_nonneg)      (ae_of_all _ (Metric.ball_subset_ball (le_of_lt hrs)))  have hgrad_bound :      ∫ x in Metric.ball x₀ s, ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2 ∂volume ≤        ∫ x in Metric.ball x₀ s, Cη ^ 2 * |positivePartSub u k x| ^ 2 ∂volume := by    refine integral_mono_ae hgrad_term_int (hpos_sq_int.const_mul (Cη ^ 2)) ?_    refine (ae_restrict_iff' (μ := volume) measurableSet_ball).2 ?_    filter_upwards with x hx    have hfd_sq_le : ‖fderiv ℝ η x‖ ^ 2 ≤ Cη ^ 2 := by      exact sq_le_sq.mpr (by        simpa [abs_of_nonneg (norm_nonneg _), abs_of_nonneg hCη] using hη_grad_bound x)    have hpos_nonneg : 0 ≤ |positivePartSub u k x| ^ 2 := by positivity    exact mul_le_mul_of_nonneg_right hfd_sq_le hpos_nonneg  have hcoeff_nonneg : 0 ≤ 4 * ellipticityRatio A := by    have hRatio_nonneg : 0 ≤ ellipticityRatio A := A.ellipticityRatio_nonneg    nlinarith  calc    ∫ x in Metric.ball x₀ r, ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume        = ∫ x in Metric.ball x₀ r, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume := hleft_eq    _ ≤ ∫ x in Metric.ball x₀ s, η x ^ 2 * ‖hw_trunc.weakGrad x‖ ^ 2 ∂volume := hleft_mono    _ ≤ (4 * ellipticityRatio A) *          ∫ x in Metric.ball x₀ s, ‖fderiv ℝ η x‖ ^ 2 * |positivePartSub u k x| ^ 2            ∂volume := hweighted    _ ≤ (4 * ellipticityRatio A) *          ∫ x in Metric.ball x₀ s, Cη ^ 2 * |positivePartSub u k x| ^ 2 ∂volume := by            exact mul_le_mul_of_nonneg_left hgrad_bound hcoeff_nonneg    _ = 4 * ellipticityRatio A * Cη ^ 2 *          ∫ x in Metric.ball x₀ s, |positivePartSub u k x| ^ 2 ∂volume := by            rw [integral_const_mul]            ring