Sobolev poincare unit Ball

theorem sobolev_poincare_unitBall    {p : ℝ} (hp : 1 < p) (hpd : p < (d : ℝ))    {u : E → ℝ}    (hw : MemW1pWitness (ENNReal.ofReal p) u (Metric.ball (0 : E) 1)) :    eLpNorm (fun x => u x - ⨍ y in Metric.ball (0 : E) 1, u y ∂volume)      (ENNReal.ofReal ((d : ℝ) * p / ((d : ℝ) - p)))      (volume.restrict (Metric.ball (0 : E) 1)) ≤    C_sobolevPoincare d p *      eLpNorm (fun x => ‖hw.weakGrad x‖) (ENNReal.ofReal p)        (volume.restrict (Metric.ball (0 : E) 1)) := by  let B := Metric.ball (0 : E) 1  let ubar := ⨍ y in B, u y ∂volume  let v : E → ℝ := fun x => u x - ubar  let pstar := ENNReal.ofReal ((d : ℝ) * p / ((d : ℝ) - p))  let hwv := memW1pWitness_sub_const_unitBall (d := d) hp hw ubar  have hwv_grad : hwv.weakGrad = hw.weakGrad :=    memW1pWitness_sub_const_unitBall_weakGrad hp hw ubar  obtain ⟨hwExt, hcpt, hagree, _hfun_bound, hgrad_bound⟩ :=    exists_unitBall_W1p_extension (d := d) hp hwv  have hW01 : MemW01p (ENNReal.ofReal p) (unitBallExtension (d := d) v) Set.univ :=    memW01p_of_memW1p_of_tsupport_subset isOpen_univ hp hwExt.memW1p hcpt      (Set.subset_univ _)  obtain ⟨hwSob, hSob⟩ := sobolev_of_memW01p_univ (d := d) (le_of_lt hp) hpd hW01  have hae_grad : hwSob.weakGrad =ᵐ[volume] hwExt.weakGrad := by    have h := MemW1pWitness.ae_eq_p (d := d) isOpen_univ (show 1 ≤ p from le_of_lt hp)      hwSob hwExt    simpa [Measure.restrict_univ] using h  have hSob' :      eLpNorm (unitBallExtension (d := d) v) pstar volume ≤        ENNReal.ofReal (C_gns d p) *          eLpNorm (fun x => ‖hwExt.weakGrad x‖) (ENNReal.ofReal p) volume := by    calc      eLpNorm (unitBallExtension (d := d) v) pstar volume          ≤ ENNReal.ofReal (C_gns d p) *              eLpNorm (fun x => ‖hwSob.weakGrad x‖) (ENNReal.ofReal p) volume := hSob      _ = ENNReal.ofReal (C_gns d p) *            eLpNorm (fun x => ‖hwExt.weakGrad x‖) (ENNReal.ofReal p) volume := by          congr 1          exact eLpNorm_congr_ae (hae_grad.fun_comp (‖·‖))  have hrestrict :      eLpNorm v pstar (volume.restrict B) ≤        eLpNorm (unitBallExtension (d := d) v) pstar volume := by    calc      eLpNorm v pstar (volume.restrict B)          = eLpNorm (unitBallExtension (d := d) v) pstar (volume.restrict B) := by            apply eLpNorm_congr_ae            have : ∀ᵐ x ∂(volume.restrict B), v x = unitBallExtension (d := d) v x := by              filter_upwards [ae_restrict_mem measurableSet_ball] with x hx              exact (hagree x hx).symm            exact this      _ ≤ eLpNorm (unitBallExtension (d := d) v) pstar volume :=          eLpNorm_mono_measure _ Measure.restrict_le_self  have hv_poinc_raw :      eLpNorm (fun x => u x - ⨍ y in B, u y ∂volume) (ENNReal.ofReal p)        (volume.restrict B) ≤      ENNReal.ofReal (C_poinc_val d) *        eLpNorm (fun x => ‖hw.weakGrad x‖) (ENNReal.ofReal p)          (volume.restrict B) :=    poincare_unitBall_W1p (d := d) hp hw  have hv_poinc :      eLpNorm v (ENNReal.ofReal p) (volume.restrict B) ≤        ENNReal.ofReal (C_poinc_val d) *          eLpNorm (fun x => ‖hwv.weakGrad x‖) (ENNReal.ofReal p)            (volume.restrict B) := by    rw [hwv_grad]    exact hv_poinc_raw  have hgrad_absorb :      eLpNorm (fun x => ‖hwExt.weakGrad x‖) (ENNReal.ofReal p) volume ≤        C_extensionGrad d p *          eLpNorm (fun x => ‖hwv.weakGrad x‖) (ENNReal.ofReal p)            (volume.restrict B) :=    extension_gradient_eLpNorm_bound (d := d) hp hwv hgrad_bound hv_poinc  have hwv_grad_eq : (fun x => ‖hwv.weakGrad x‖) = (fun x => ‖hw.weakGrad x‖) := by    ext x    rw [hwv_grad]  calc    eLpNorm v pstar (volume.restrict B)        ≤ eLpNorm (unitBallExtension (d := d) v) pstar volume := hrestrict    _ ≤ ENNReal.ofReal (C_gns d p) *          eLpNorm (fun x => ‖hwExt.weakGrad x‖) (ENNReal.ofReal p) volume := hSob'    _ ≤ ENNReal.ofReal (C_gns d p) *          (C_extensionGrad d p *            eLpNorm (fun x => ‖hwv.weakGrad x‖) (ENNReal.ofReal p)              (volume.restrict B)) := by          gcongr    _ = ENNReal.ofReal (C_gns d p) * C_extensionGrad d p *          eLpNorm (fun x => ‖hwv.weakGrad x‖) (ENNReal.ofReal p)            (volume.restrict B) := by          rw [mul_assoc]    _ = C_sobolevPoincare d p *          eLpNorm (fun x => ‖hwv.weakGrad x‖) (ENNReal.ofReal p)            (volume.restrict B) := by          rfl    _ = C_sobolevPoincare d p *          eLpNorm (fun x => ‖hw.weakGrad x‖) (ENNReal.ofReal p)            (volume.restrict B) := by          rw [hwv_grad_eq]