Smooth input unit Ball Extension smoothing

theorem smooth_input_unitBallExtension_smoothing    {p : ℝ} (hp : 1 < p) {ψ : E → ℝ}    (hψ_smooth : ContDiff ℝ (⊤ : ℕ∞) ψ)    (_hψ_cpt : HasCompactSupport ψ) :    ∃ Gψ : E → E,      MemLp (unitBallExtension (d := d) ψ) (ENNReal.ofReal p) volume ∧      (∀ i : Fin d, MemLp (fun x => Gψ x i) (ENNReal.ofReal p) volume) ∧      (∫⁻ x, (ENNReal.ofReal |unitBallExtension (d := d) ψ x|) ^ p ∂volume)        ≤ C_unitBallExtensionFun d *          ∫⁻ x in Metric.ball (0 : E) 1, (ENNReal.ofReal |ψ x|) ^ p ∂volume ∧      (∫⁻ x, (ENNReal.ofReal ‖Gψ x‖) ^ p ∂volume)        ≤ (∫⁻ x in Metric.ball (0 : E) 1, (ENNReal.ofReal ‖fderiv ℝ ψ x‖) ^ p ∂volume) +          C_unitBallExtensionGrad d p *            (∫⁻ x in Metric.ball (0 : E) 1, (ENNReal.ofReal |ψ x|) ^ p ∂volume +             ∫⁻ x in Metric.ball (0 : E) 1, (ENNReal.ofReal ‖fderiv ℝ ψ x‖) ^ p ∂volume) ∧      ∃ Φ : ℕ → E → ℝ,        (∀ n, ContDiff ℝ (⊤ : ℕ∞) (Φ n)) ∧        (∀ n, HasCompactSupport (Φ n)) ∧        Tendsto          (fun n =>            eLpNorm (fun x => Φ n x - unitBallExtension (d := d) ψ x)              (ENNReal.ofReal p) volume)          atTop (nhds 0) ∧        ∀ i : Fin d,          Tendsto            (fun n =>              eLpNorm                (fun x => (fderiv ℝ (Φ n) x) (EuclideanSpace.single i 1) - Gψ x i)                (ENNReal.ofReal p) volume)            atTop (nhds 0) := by  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 huExt_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    have hTmp := hΦ0_memLp.sub hDiff_memLp    exact memLp_congr_ae (Filter.Eventually.of_forall fun x => by simp [sub_sub_cancel]) |>.mp hTmp  have hGψ_memLp : ∀ i : Fin d,      MemLp (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) i)        (ENNReal.ofReal p) volume := by    intro i    have hderiv_memLp :        MemLp          (fun x => (fderiv ℝ (smoothUnitBallExtensionApprox (d := d) (unitBallApproxEps 0) ψ) x)            (EuclideanSpace.single i 1))          (ENNReal.ofReal p) volume := by      have hderiv_smooth :          ContDiff ℝ (⊤ : ℕ∞)            (fun x => (fderiv ℝ (smoothUnitBallExtensionApprox (d := d) (unitBallApproxEps 0) ψ) x)              (EuclideanSpace.single i 1)) :=        (hΦ_smooth 0).fderiv_right (m := (⊤ : ℕ∞)) (by simp)          |>.clm_apply contDiff_const      exact hderiv_smooth.continuous.memLp_of_hasCompactSupport        ((hΦ_cpt 0).fderiv_apply (𝕜 := ℝ) _)    have hDiff_memLp :=      memLp_fderiv_smoothUnitBallExtensionApprox_sub_exactGradApply (d := d) hp hψ_smooth 0 i    have hTmp := hderiv_memLp.sub hDiff_memLp    exact memLp_congr_ae (Filter.Eventually.of_forall fun x => by      simp [sub_sub_cancel, exactUnitBallExtensionGrad,        SmoothApproximationInternal.exactUnitBallExtensionGrad, exactUnitBallExtensionGradApply])      |>.mp hTmp  have hweak :      ∀ i : Fin d, HasWeakPartialDeriv i        (fun x => (exactUnitBallExtensionGrad (d := d) ψ x) i)        (unitBallExtension (d := d) ψ) Set.univ := by    have hΦ_tendsto_fun :=      tendsto_eLpNorm_smoothUnitBallExtensionApprox_sub_unitBallExtension (d := d) hp hψ_smooth    have hΦ_tendsto_grad :=      tendsto_eLpNorm_fderiv_smoothUnitBallExtensionApprox_sub_exactGradApply (d := d) hp hψ_smooth    exact hasWeakPartials_of_global_smoothApprox (d := d) hp huExt_memLp hGψ_memLp      hΦ_smooth hΦ_cpt hΦ_tendsto_fun (fun i => by        convert hΦ_tendsto_grad i using 2)  let hwExt : MemW1pWitness (ENNReal.ofReal p)      (unitBallExtension (d := d) ψ) Set.univ :=    { memLp := by rw [Measure.restrict_univ]; exact huExt_memLp      weakGrad := exactUnitBallExtensionGrad (d := d) ψ      weakGrad_component_memLp := by        intro i; rw [Measure.restrict_univ]; exact hGψ_memLp i      isWeakGrad := hweak }  rcases exists_global_smooth_W1p_approx_of_localizedWitness      (d := d) (Ω := Set.univ) isOpen_univ hp hwExt      (unitBallExtension_hasCompactSupport (d := d) ψ) (Set.subset_univ _) with    ⟨Ψ, hΨ_smooth, hΨ_cpt, hΨ_fun, hΨ_grad⟩  have hψ_smooth1 : ContDiff ℝ 1 ψ := hψ_smooth.of_le (by simp)  have hest := smooth_unitBallExtension_W1p_estimate (d := d) (p := p) hp.le hψ_smooth1  have hfun_bound :      (∫⁻ x, (ENNReal.ofReal |unitBallExtension (d := d) ψ x|) ^ p ∂volume)        ≤ C_unitBallExtensionFun d *          ∫⁻ x in Metric.ball (0 : E) 1, (ENNReal.ofReal |ψ x|) ^ p ∂volume := by    have hfun_support :        (fun x => (ENNReal.ofReal |unitBallExtension (d := d) ψ x|) ^ p) =          (Metric.ball (0 : E) 2).indicator            (fun x => (ENNReal.ofReal |unitBallExtension (d := d) ψ x|) ^ p) := by      funext x      by_cases hx : x ∈ Metric.ball (0 : E) 2      · simp [hx]      · have hnorm : 2 ≤ ‖x‖ := by          simp only [Metric.mem_ball, dist_zero_right, not_lt] at hx; exact hx        have hzero := unitBallExtension_eq_zero_of_two_le_norm (d := d) (u := ψ) hnorm        simp only [hzero, abs_zero, ENNReal.ofReal_zero, Set.indicator_of_notMem hx,          ENNReal.zero_rpow_of_pos (show (0 : ℝ) < p by linarith)]    rw [hfun_support, lintegral_indicator Metric.isOpen_ball.measurableSet]    exact hest.1  have hgrad_bound := exactUnitBallExtensionGrad_bound (d := d) hp hψ_smooth  refine ⟨exactUnitBallExtensionGrad (d := d) ψ,    huExt_memLp, hGψ_memLp, hfun_bound, hgrad_bound,    Ψ, hΨ_smooth, hΨ_cpt, hΨ_fun, ?_⟩  intro i  have h := hΨ_grad i  refine (Filter.tendsto_congr fun n => eLpNorm_congr_ae ?_).mpr h  filter_upwards with x; simp [hwExt]