Sobolev prepare on ball

theorem sobolev_prepare_on_ball    {x₀ : E} {s : ℝ} {v : E → ℝ}    (hd : 2 < (d : ℝ))    (_hs : 0 < s)    (hvW01 : MemW01p 2 v (Metric.ball x₀ s))    (hv_support : tsupport v ⊆ Metric.ball x₀ s) :    ∃ hwv_real :      MemW1pWitness (ENNReal.ofReal (2 : ℝ)) v (Metric.ball x₀ s),      eLpNorm v          (ENNReal.ofReal ((d : ℝ) * 2 / ((d : ℝ) - 2)))          (volume.restrict (Metric.ball x₀ s)) ≤        ENNReal.ofReal (C_gns d 2) *          eLpNorm (fun x => ‖hwv_real.weakGrad x‖) 2            (volume.restrict (Metric.ball x₀ s)) := by  classical  let Ω : Set E := Metric.ball x₀ s  let μ : Measure E := volume.restrict Ω  have hΩ_open : IsOpen Ω := by    simp [Ω]  have hΩ_meas : MeasurableSet Ω := measurableSet_ball  haveI : IsFiniteMeasure μ := by    dsimp [μ, Ω]    rw [isFiniteMeasure_restrict]    exact measure_ball_lt_top.ne  let hwv : MemW1pWitness 2 v Ω := Classical.choose hvW01.2  have hv_indicator_eq : Ω.indicator v = v := by    ext x    by_cases hx : x ∈ Ω    · simp [hx]    · have hvx0 : v x = 0 := by        exact image_eq_zero_of_notMem_tsupport (fun hxt => hx (hv_support hxt))      simp [hx, hvx0]  have hvW01_real : MemW01p (ENNReal.ofReal (2 : ℝ)) v Ω := by    simpa using hvW01  have hwv_real : MemW1pWitness (ENNReal.ofReal (2 : ℝ)) v Ω := by    simpa using hwv  let hwv_univ_raw :      MemW1pWitness (ENNReal.ofReal (2 : ℝ)) (Ω.indicator v) Set.univ :=    zeroExtend_memW1pWitness_p (d := d) hΩ_open (p := 2) (by norm_num) hvW01_real hwv_real  let hwv_univ : MemW1pWitness (ENNReal.ofReal (2 : ℝ)) v Set.univ :=    { memLp := by        simpa [hv_indicator_eq] using hwv_univ_raw.memLp      weakGrad := hwv_univ_raw.weakGrad      weakGrad_component_memLp := hwv_univ_raw.weakGrad_component_memLp      isWeakGrad := by        simpa [hv_indicator_eq] using hwv_univ_raw.isWeakGrad }  have hvW01_univ : MemW01p (ENNReal.ofReal (2 : ℝ)) v Set.univ := by    simpa [hv_indicator_eq] using      zeroExtend_memW01p_p (d := d) hΩ_open (p := 2) (by norm_num) hvW01_real  let qexp := ENNReal.ofReal ((d : ℝ) * 2 / ((d : ℝ) - 2))  obtain ⟨hwSob, hSob⟩ :=    sobolev_of_memW01p_univ (d := d) (p := 2) (u := v) (by norm_num) hd hvW01_univ  have hae_grad :      hwSob.weakGrad =ᵐ[volume] hwv_univ.weakGrad := by    simpa [Measure.restrict_univ] using      MemW1pWitness.ae_eq_p (d := d) isOpen_univ (p := 2) (by norm_num) hwSob hwv_univ  have hSob' :      eLpNorm v qexp volume ≤        ENNReal.ofReal (C_gns d 2) *          eLpNorm (fun x => ‖hwv_univ.weakGrad x‖) 2 volume := by    calc      eLpNorm v qexp volume          ≤ ENNReal.ofReal (C_gns d 2) *              eLpNorm (fun x => ‖hwSob.weakGrad x‖) 2 volume := by                simpa [qexp] using hSob      _ = ENNReal.ofReal (C_gns d 2) *            eLpNorm (fun x => ‖hwv_univ.weakGrad x‖) 2 volume := by          congr 1          exact eLpNorm_congr_ae (hae_grad.fun_comp (‖·‖))  have hgrad_ext_vec :      hwv_univ.weakGrad = Ω.indicator hwv_real.weakGrad := by    ext x i    by_cases hx : x ∈ Ω    · simp [hwv_univ, hwv_univ_raw, zeroExtend_memW1pWitness_p, hx]    · simp [hwv_univ, hwv_univ_raw, zeroExtend_memW1pWitness_p, hx]  have hgrad_ext :      (fun x => ‖hwv_univ.weakGrad x‖) = Ω.indicator (fun x => ‖hwv_real.weakGrad x‖) := by    ext x    by_cases hx : x ∈ Ω    · simp [hgrad_ext_vec, hx]    · simp [hgrad_ext_vec, hx]  have hgrad_restrict :      eLpNorm (fun x => ‖hwv_univ.weakGrad x‖) 2 volume =        eLpNorm (fun x => ‖hwv_real.weakGrad x‖) 2 μ := by    rw [hgrad_ext, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict hΩ_meas]  have hv_support_fun : Function.support v ⊆ Ω := by    intro x hx    exact hv_support (subset_tsupport _ hx)  have hv_restrict :      eLpNorm v qexp μ = eLpNorm v qexp volume := by    simpa [μ] using      (MeasureTheory.eLpNorm_restrict_eq_of_support_subset        (μ := volume) (p := qexp) hv_support_fun)  have hSob'' :      eLpNorm v qexp μ ≤        ENNReal.ofReal (C_gns d 2) * eLpNorm (fun x => ‖hwv_real.weakGrad x‖) 2 μ := by    calc      eLpNorm v qexp μ = eLpNorm v qexp volume := hv_restrict      _ ≤ ENNReal.ofReal (C_gns d 2) *            eLpNorm (fun x => ‖hwv_univ.weakGrad x‖) 2 volume := hSob'      _ = ENNReal.ofReal (C_gns d 2) * eLpNorm (fun x => ‖hwv_real.weakGrad x‖) 2 μ := by            rw [hgrad_restrict]  exact ⟨hwv_real, hSob''⟩