Weak Grad component cauchy bound

theorem weakGrad_component_cauchy_bound    {p : ℝ} (hp : 1 < p)    {ψ₁ ψ₂ : E → ℝ}    (_hψ₁_smooth : ContDiff ℝ (⊤ : ℕ∞) ψ₁) (_hψ₂_smooth : ContDiff ℝ (⊤ : ℕ∞) ψ₂)    (_hψ₁_cpt : HasCompactSupport ψ₁) (_hψ₂_cpt : HasCompactSupport ψ₂)    {G₁ G₂ : E → E} {i : Fin d}    (_hG₁_wd : HasWeakPartialDeriv i (fun x => G₁ x i)        (unitBallExtension (d := d) ψ₁) Set.univ)    (_hG₂_wd : HasWeakPartialDeriv i (fun x => G₂ x i)        (unitBallExtension (d := d) ψ₂) Set.univ)    (_hG₁_memLp : MemLp (fun x => G₁ x i) (ENNReal.ofReal p) volume)    (_hG₂_memLp : MemLp (fun x => G₂ x i) (ENNReal.ofReal p) volume) :    ∫⁻ x, (ENNReal.ofReal |G₁ x i - G₂ x i|) ^ p ∂volume ≤      ∫⁻ x, (ENNReal.ofReal ‖exactUnitBallExtensionGrad (d := d) (fun x => ψ₁ x - ψ₂ x) x‖) ^ p        ∂volume := by  set ψ : E → ℝ := fun x => ψ₁ x - ψ₂ x with hψ_def  have hψ_smooth : ContDiff ℝ (⊤ : ℕ∞) ψ := _hψ₁_smooth.sub _hψ₂_smooth  have hp_enn : (1 : ℝ≥0∞) ≤ ENNReal.ofReal p := by    simpa using ENNReal.ofReal_le_ofReal hp.le  have hGdiff_wd : HasWeakPartialDeriv i (fun x => G₁ x i - G₂ x i)      (unitBallExtension (d := d) ψ) Set.univ := by    intro φ hφ hφ_supp hφ_tsupport    have h1 := _hG₁_wd φ hφ hφ_supp hφ_tsupport    have h2 := _hG₂_wd φ hφ hφ_supp hφ_tsupport    let ei : E := EuclideanSpace.single i (1 : ℝ)    have hderiv_cont : Continuous (fun x => (fderiv ℝ φ x) ei) :=      (hφ.continuous_fderiv (by simp : ((⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0)).clm_apply        continuous_const    have hderiv_supp : HasCompactSupport (fun x => (fderiv ℝ φ x) ei) :=      hφ_supp.fderiv_apply (𝕜 := ℝ) ei    have hG₁_loc : LocallyIntegrable (fun x => G₁ x i) (volume.restrict Set.univ) := by      rw [Measure.restrict_univ]; exact _hG₁_memLp.locallyIntegrable hp_enn    have hG₂_loc : LocallyIntegrable (fun x => G₂ x i) (volume.restrict Set.univ) := by      rw [Measure.restrict_univ]; exact _hG₂_memLp.locallyIntegrable hp_enn    have hG₁_int : Integrable (fun x => G₁ x i * φ x) (volume.restrict Set.univ) := by      simpa [smul_eq_mul] using        hG₁_loc.integrable_smul_right_of_hasCompactSupport hφ.continuous hφ_supp    have hG₂_int : Integrable (fun x => G₂ x i * φ x) (volume.restrict Set.univ) := by      simpa [smul_eq_mul] using        hG₂_loc.integrable_smul_right_of_hasCompactSupport hφ.continuous hφ_supp    have hLHS : ∀ x, unitBallExtension (d := d) ψ x * (fderiv ℝ φ x) ei =        unitBallExtension (d := d) ψ₁ x * (fderiv ℝ φ x) ei -        unitBallExtension (d := d) ψ₂ x * (fderiv ℝ φ x) ei := by      intro x; simp only [hψ_def, unitBallExtension_sub (d := d) ψ₁ ψ₂]; ring    have hψ₁_memLp : MemLp (unitBallExtension (d := d) ψ₁) (ENNReal.ofReal p) volume := by      rcases smooth_input_unitBallExtension_smoothing (d := d) hp _hψ₁_smooth _hψ₁_cpt with        ⟨_, hml, _⟩; exact hml    have hψ₂_memLp : MemLp (unitBallExtension (d := d) ψ₂) (ENNReal.ofReal p) volume := by      rcases smooth_input_unitBallExtension_smoothing (d := d) hp _hψ₂_smooth _hψ₂_cpt with        ⟨_, hml, _⟩; exact hml    have hψ₁_loc : LocallyIntegrable (unitBallExtension (d := d) ψ₁)        (volume.restrict Set.univ) := by      rw [Measure.restrict_univ]; exact hψ₁_memLp.locallyIntegrable hp_enn    have hψ₂_loc : LocallyIntegrable (unitBallExtension (d := d) ψ₂)        (volume.restrict Set.univ) := by      rw [Measure.restrict_univ]; exact hψ₂_memLp.locallyIntegrable hp_enn    have hψ₁_int : Integrable (fun x => unitBallExtension (d := d) ψ₁ x * (fderiv ℝ φ x) ei)        (volume.restrict Set.univ) := by      simpa [smul_eq_mul, mul_comm] using        hψ₁_loc.integrable_smul_right_of_hasCompactSupport hderiv_cont hderiv_supp    have hψ₂_int : Integrable (fun x => unitBallExtension (d := d) ψ₂ x * (fderiv ℝ φ x) ei)        (volume.restrict Set.univ) := by      simpa [smul_eq_mul, mul_comm] using        hψ₂_loc.integrable_smul_right_of_hasCompactSupport hderiv_cont hderiv_supp    calc ∫ x in Set.univ,          unitBallExtension (d := d) ψ x * (fderiv ℝ φ x) ei        = ∫ x in Set.univ, (unitBallExtension (d := d) ψ₁ x * (fderiv ℝ φ x) ei -            unitBallExtension (d := d) ψ₂ x * (fderiv ℝ φ x) ei) := by          congr 1; ext x; exact hLHS x      _ = (∫ x in Set.univ, unitBallExtension (d := d) ψ₁ x * (fderiv ℝ φ x) ei) -          (∫ x in Set.univ, unitBallExtension (d := d) ψ₂ x * (fderiv ℝ φ x) ei) :=          integral_sub hψ₁_int hψ₂_int      _ = (-∫ x in Set.univ, G₁ x i * φ x) - (-∫ x in Set.univ, G₂ x i * φ x) := by          rw [h1, h2]      _ = -∫ x in Set.univ, (G₁ x i - G₂ x i) * φ x := by          have hsub := (integral_sub hG₁_int hG₂_int).symm          have hfun : (fun x => G₁ x i * φ x - G₂ x i * φ x) =              (fun x => (G₁ x i - G₂ x i) * φ x) := by funext x; ring          linarith [hsub, hfun ▸ hsub]  have hΦ_smooth_ψ : ∀ n, ContDiff ℝ (⊤ : ℕ∞)      (smoothUnitBallExtensionApprox (d := d) (unitBallApproxEps n) ψ) :=    fun n => smoothUnitBallExtensionApprox_contDiff (d := d) (unitBallApproxEps_pos n)      (unitBallApproxEps_lt_one n) hψ_smooth  have hΦ_cpt_ψ : ∀ n, HasCompactSupport      (smoothUnitBallExtensionApprox (d := d) (unitBallApproxEps n) ψ) :=    fun n => smoothUnitBallExtensionApprox_hasCompactSupport (d := d) (ψ := ψ)      (unitBallApproxEps_pos n)  have hExt_memLp : MemLp (unitBallExtension (d := d) ψ) (ENNReal.ofReal p) volume := by    have hΦ0_memLp : MemLp (smoothUnitBallExtensionApprox (d := d) (unitBallApproxEps 0) ψ)        (ENNReal.ofReal p) (volume : Measure E) :=      (hΦ_smooth_ψ 0).continuous.memLp_of_hasCompactSupport (hΦ_cpt_ψ 0)    have hDiff_memLp :=      memLp_smoothUnitBallExtensionApprox_sub_unitBallExtension (d := d) hp hψ_smooth 0    exact memLp_congr_ae (Filter.Eventually.of_forall fun x => by      simp [sub_sub_cancel]) |>.mp (hΦ0_memLp.sub hDiff_memLp)  have hGψ_memLp : ∀ j : Fin d,      MemLp (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) j)        (ENNReal.ofReal p) volume := by    intro j    have hderiv_memLp :        MemLp (fun x => (fderiv ℝ (smoothUnitBallExtensionApprox (d := d)            (unitBallApproxEps 0) ψ) x) (EuclideanSpace.single j 1))          (ENNReal.ofReal p) volume := by      exact ((hΦ_smooth_ψ 0).fderiv_right (m := (⊤ : ℕ∞)) (by simp)        |>.clm_apply contDiff_const).continuous.memLp_of_hasCompactSupport          ((hΦ_cpt_ψ 0).fderiv_apply (𝕜 := ℝ) _)    have hDiff_memLp :=      memLp_fderiv_smoothUnitBallExtensionApprox_sub_exactGradApply        (d := d) hp hψ_smooth 0 j    exact memLp_congr_ae (Filter.Eventually.of_forall fun x => by      simp [sub_sub_cancel, exactUnitBallExtensionGrad,        SmoothApproximationInternal.exactUnitBallExtensionGrad, exactUnitBallExtensionGradApply])        |>.mp (hderiv_memLp.sub hDiff_memLp)  have hExact_wd : HasWeakPartialDeriv i      (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) i)      (unitBallExtension (d := d) ψ) Set.univ :=    hasWeakPartials_of_global_smoothApprox (d := d) hp hExt_memLp hGψ_memLp      hΦ_smooth_ψ hΦ_cpt_ψ      (tendsto_eLpNorm_smoothUnitBallExtensionApprox_sub_unitBallExtension        (d := d) hp hψ_smooth)      (fun j => by        convert tendsto_eLpNorm_fderiv_smoothUnitBallExtensionApprox_sub_exactGradApply          (d := d) hp hψ_smooth j using 2) i  have hGdiff_loc : LocallyIntegrable (fun x => G₁ x i - G₂ x i)      (volume.restrict Set.univ) := by    rw [Measure.restrict_univ]    exact (_hG₁_memLp.sub _hG₂_memLp).locallyIntegrable hp_enn  have hExact_loc : LocallyIntegrable      (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) i)      (volume.restrict Set.univ) := by    rw [Measure.restrict_univ]; exact (hGψ_memLp i).locallyIntegrable hp_enn  have hae : (fun x => G₁ x i - G₂ x i) =ᵐ[volume.restrict Set.univ]      (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) i) :=    HasWeakPartialDeriv.ae_eq isOpen_univ hGdiff_wd hExact_wd hGdiff_loc hExact_loc  rw [Measure.restrict_univ] at hae  calc ∫⁻ x, (ENNReal.ofReal |G₁ x i - G₂ x i|) ^ p ∂volume      = ∫⁻ x, (ENNReal.ofReal |(exactUnitBallExtensionGrad (d := d) ψ x) i|) ^ p          ∂volume := by        apply lintegral_congr_ae        filter_upwards [hae] with x hx; rw [hx]    _ ≤ ∫⁻ x, (ENNReal.ofReal ‖exactUnitBallExtensionGrad (d := d) ψ x‖) ^ p          ∂volume :=        lintegral_rpow_abs_component_le_lintegral_rpow_norm (d := d) (by linarith) i