Sobolev of approx

theorem sobolev_of_approx {p : ℝ} (hp : 1 ≤ p) (hpd : p < (d : ℝ))    {u : E → ℝ} {G : E → E}    (hu_aesm : AEStronglyMeasurable u volume)    (hG_comp_aesm : ∀ i : Fin d, AEStronglyMeasurable (fun x => G x i) volume)    (φ : ℕ → E → ℝ)    (hφ_smooth : ∀ n, ContDiff ℝ (⊤ : ℕ∞) (φ n))    (hφ_cpt : ∀ n, HasCompactSupport (φ n))    (hφ_fun : Tendsto (fun n => eLpNorm (fun x => φ n x - u x) (ENNReal.ofReal p) volume)      atTop (nhds 0))    (hφ_grad : ∀ 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)) :    eLpNorm u (ENNReal.ofReal ((d : ℝ) * p / ((d : ℝ) - p))) volume ≤    ENNReal.ofReal (C_gns d p) *      eLpNorm (fun x => ‖G x‖) (ENNReal.ofReal p) volume := by  set p_star := ENNReal.ofReal ((d : ℝ) * p / ((d : ℝ) - p)) with hp_star_def  set p_enn := ENNReal.ofReal p with hp_enn_def  set C := ENNReal.ofReal (C_gns d p) with hC_def  have hGNS : ∀ n,      eLpNorm (φ n) p_star volume ≤      C * eLpNorm (fderiv ℝ (φ n)) p_enn volume :=    fun n => sobolev_smooth hp hpd ((hφ_smooth n).of_le (by norm_cast)) (hφ_cpt n)  have hφ_aesm : ∀ n, AEStronglyMeasurable (φ n) volume :=    fun n => (hφ_smooth n).continuous.aestronglyMeasurable  have hp_ne : p_enn ≠ 0 := by    simp [p_enn]    linarith  have hp_one_enn : (1 : ℝ≥0∞) ≤ p_enn := by    rw [hp_enn_def, ← ENNReal.ofReal_one]    exact ENNReal.ofReal_le_ofReal hp  have hTIM : TendstoInMeasure volume φ atTop u :=    tendstoInMeasure_of_eLpNorm_tendsto hp_ne hφ_aesm hu_aesm hφ_fun  obtain ⟨σ, hσ_mono, hσ_ae⟩ := hTIM.exists_seq_tendsto_ae  have hFatou : eLpNorm u p_star volume ≤      atTop.liminf (fun n => eLpNorm (φ (σ n)) p_star volume) :=    Lp.eLpNorm_lim_le_liminf_eLpNorm (fun n => hφ_aesm (σ n)) u hσ_ae  let gradVec : ℕ → E → E := fun n x =>    WithLp.toLp 2 (fun i => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1))  have hBridge : ∀ n, (fun x => ‖fderiv ℝ (φ n) x‖) =ᵐ[volume]      (fun x => ‖gradVec n x‖) := by    intro n    filter_upwards with x    exact norm_fderiv_eq_norm_partials  have hGNS' : ∀ n,      eLpNorm (φ n) p_star volume ≤      C * eLpNorm (fun x => ‖gradVec n x‖) p_enn volume := by    intro n    calc      eLpNorm (φ n) p_star volume        ≤ C * eLpNorm (fderiv ℝ (φ n)) p_enn volume := hGNS n      _ = C * eLpNorm (fun x => ‖gradVec n x‖) p_enn volume := by          congr 1          rw [← eLpNorm_norm (fderiv ℝ (φ n))]          exact eLpNorm_congr_ae (hBridge n)  have hGradDiffTendstoZero : Tendsto      (fun n => eLpNorm (fun x => gradVec n x - G x) p_enn volume) atTop (nhds 0) := by    have hNormCompTendsto :=      partialDiff_sum_tendsto_zero (p := p) (φ := φ) (G := G) hφ_grad    have hBound :        ∀ᶠ n in atTop,          eLpNorm (fun x => gradVec n x - G x) p_enn volume ≤            ∑ i : Fin d,              eLpNorm                (fun x => (fderiv ℝ (φ n) x) (EuclideanSpace.single i 1) - G x i)                p_enn volume := by      apply Eventually.of_forall      intro n      simpa [gradVec, hp_enn_def] using        gradVec_eLpNorm_le_sum (p := p) (φ := φ) (G := G) hp hφ_smooth hG_comp_aesm n    have hZeroLE :        ∀ᶠ n in atTop, (0 : ℝ≥0∞) ≤ eLpNorm (fun x => gradVec n x - G x) p_enn volume :=      Eventually.of_forall fun n => zero_le _    exact tendsto_of_tendsto_of_tendsto_of_le_of_le'      (show Tendsto (fun _ : ℕ => (0 : ℝ≥0∞)) atTop (nhds 0) from tendsto_const_nhds)      hNormCompTendsto      hZeroLE      hBound  have hBound : atTop.liminf (fun n => eLpNorm (φ (σ n)) p_star volume) ≤      C * eLpNorm (fun x => ‖G x‖) p_enn volume := by    have hC_ne_top : C ≠ ⊤ := ENNReal.ofReal_ne_top    have hGnorm_aesm : AEStronglyMeasurable (fun x => ‖G x‖) volume := by      exact (aestronglyMeasurable_euclidean_of_components hG_comp_aesm).norm    have hGradNormUpper :        ∀ᶠ n in atTop,          eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume ≤            eLpNorm (fun x => ‖G x‖) p_enn volume +              eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume := by      apply Eventually.of_forall      intro n      have hGradNormAesm :          AEStronglyMeasurable (fun x => ‖gradVec (σ n) x‖ - ‖G x‖) volume := by        have hGradVecCont : Continuous (gradVec (σ n)) := by          have h_toLp_cont : Continuous (fun x : Fin d → ℝ => WithLp.toLp 2 x) := by            simpa using (PiLp.continuous_toLp 2 (fun _ : Fin d => ℝ))          refine h_toLp_cont.comp ?_          rw [continuous_pi_iff]          intro i          exact ((hφ_smooth (σ n)).continuous_fderiv (by simp)).clm_apply continuous_const        have hGradVecAesm : AEStronglyMeasurable (gradVec (σ n)) volume :=          hGradVecCont.aestronglyMeasurable        exact hGradVecAesm.norm.sub hGnorm_aesm      have hNormDiff :          eLpNorm (fun x => ‖gradVec (σ n) x‖ - ‖G x‖) p_enn volume ≤            eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume := by        calc          eLpNorm (fun x => ‖gradVec (σ n) x‖ - ‖G x‖) p_enn volume              = eLpNorm (fun x => |‖gradVec (σ n) x‖ - ‖G x‖|) p_enn volume := by                  simpa [Real.norm_eq_abs] using                    (eLpNorm_norm                      (f := fun x => ‖gradVec (σ n) x‖ - ‖G x‖)                      (p := p_enn) (μ := volume)).symm          _ ≤ eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume := by                refine eLpNorm_mono_ae ?_                filter_upwards with x                simpa [Real.norm_eq_abs] using                  (abs_norm_sub_norm_le (gradVec (σ n) x) (G x))      calc        eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume            = eLpNorm (fun x => (‖gradVec (σ n) x‖ - ‖G x‖) + ‖G x‖) p_enn volume := by                congr 1                ext x                ring        _ ≤ eLpNorm (fun x => ‖gradVec (σ n) x‖ - ‖G x‖) p_enn volume +              eLpNorm (fun x => ‖G x‖) p_enn volume := by                exact eLpNorm_add_le hGradNormAesm hGnorm_aesm hp_one_enn        _ ≤ eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume +              eLpNorm (fun x => ‖G x‖) p_enn volume := by                exact add_le_add hNormDiff le_rfl        _ = eLpNorm (fun x => ‖G x‖) p_enn volume +              eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume := by                rw [add_comm]    have hGradBound :        atTop.liminf (fun n => C * eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume) ≤          C * eLpNorm (fun x => ‖G x‖) p_enn volume := by      have hDiffZeroSubseq :          Tendsto            (fun n => C * eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume)            atTop (nhds 0) := by          simpa using            (ENNReal.Tendsto.const_mul              (hGradDiffTendstoZero.comp hσ_mono.tendsto_atTop)              (Or.inr hC_ne_top))      have hu_grad :          atTop.IsBoundedUnder (· ≥ ·)            (fun n => C * eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume) :=        isBoundedUnder_of_eventually_ge (a := 0) <| Eventually.of_forall fun _ => by simp      have hv_rhs :          atTop.IsCoboundedUnder (· ≥ ·)            (fun n =>              C * eLpNorm (fun x => ‖G x‖) p_enn volume +                C * eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume) :=        isCoboundedUnder_ge_of_eventually_le atTop <|          Eventually.of_forall fun _ => le_top      calc        atTop.liminf (fun n => C * eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume)            ≤ atTop.liminf                (fun n =>                  C * eLpNorm (fun x => ‖G x‖) p_enn volume +                    C * eLpNorm (fun x => gradVec (σ n) x - G x) p_enn volume) := by                  exact Filter.liminf_le_liminf                    (hGradNormUpper.mono fun n hn => by                      simpa [mul_add, add_comm, add_left_comm, add_assoc] using                        mul_le_mul_right hn C)                    hu_grad hv_rhs        _ = atTop.liminf (fun _ : ℕ => C * eLpNorm (fun x => ‖G x‖) p_enn volume) := by              simpa using                ENNReal.liminf_add_of_right_tendsto_zero hDiffZeroSubseq                  (fun _ : ℕ => C * eLpNorm (fun x => ‖G x‖) p_enn volume)        _ = C * eLpNorm (fun x => ‖G x‖) p_enn volume := by              simp    have hu_phi :        atTop.IsBoundedUnder (· ≥ ·) (fun n => eLpNorm (φ (σ n)) p_star volume) :=      isBoundedUnder_of_eventually_ge (a := 0) <| Eventually.of_forall fun _ => by simp    have hv_grad :        atTop.IsCoboundedUnder (· ≥ ·)          (fun n => C * eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume) :=      isCoboundedUnder_ge_of_eventually_le atTop <|        Eventually.of_forall fun _ => le_top    calc      atTop.liminf (fun n => eLpNorm (φ (σ n)) p_star volume)          ≤ atTop.liminf (fun n => C * eLpNorm (fun x => ‖gradVec (σ n) x‖) p_enn volume) := by            exact Filter.liminf_le_liminf              (Eventually.of_forall fun n => hGNS' (σ n))              hu_phi hv_grad      _ ≤ C * eLpNorm (fun x => ‖G x‖) p_enn volume := hGradBound  exact le_trans hFatou hBound