Exact source: MathlibAnnex/Analysis/Normed/Plucker/BoundaryExtension.lean
Pinned GitHub source · Raw UTF-8 source
Back to One boundary extension with all five analytic properties · Back to A target contraction generator lies in the source body
1import MathlibAnnex.Analysis.Normed.Plucker.Average2import MathlibAnnex.Analysis.Normed.Sphere.Basic3import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport4import Mathlib.Topology.MetricSpace.Lipschitz56/-!7# Boundary extensions with a derivative average in the Plücker body89Finite-coordinate McShane extension is performed in the norm of `Space M`.10The reference coordinates retain their original norm and Lebesgue measure.11The public existence theorem retains every field of the private witness.12-/1314noncomputable section1516open Set MeasureTheory17open MathlibAnnex.EquivalentSeminorm1819namespace MathlibAnnex.Plucker2021namespace Internal2223private def modelBoundaryAmbient {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))24 (g : M.unitSphere → (Fin N → ℝ)) : Space M → (Fin N → ℝ) :=25 fun x => if hx : M.p (show Fin n → ℝ from x) = 1 then g ⟨_, hx⟩ else 02627private theorem lipschitzOnWith_modelBoundaryAmbient {n N : ℕ}28 (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ))29 (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :30 LipschitzOnWith 1 (modelBoundaryAmbient M g) (Metric.sphere (0 : Space M) 1) := by31 refine LipschitzOnWith.mk_one ?_32 intro x hx y hy33 have hx' : M.p (show Fin n → ℝ from x) = 1 := mem_sphere_zero_iff_norm.mp hx34 have hy' : M.p (show Fin n → ℝ from y) = 1 := mem_sphere_zero_iff_norm.mp hy35 have hxy := hg ⟨(show Fin n → ℝ from x), hx'⟩ ⟨(show Fin n → ℝ from y), hy'⟩36 calc37 dist (modelBoundaryAmbient M g x) (modelBoundaryAmbient M g y) =38 ‖g ⟨(show Fin n → ℝ from x), hx'⟩ -39 g ⟨(show Fin n → ℝ from y), hy'⟩‖ := by40 simp [modelBoundaryAmbient, hx', hy', dist_eq_norm]41 _ ≤ M.p ((show Fin n → ℝ from x) - (show Fin n → ℝ from y)) := hxy42 _ = dist x y := (M.dist_space_eq x y).symm4344private def modelMcShaneToCoord {n N : ℕ} (M : EquivalentSeminorm (Fin n → ℝ))45 (g : M.unitSphere → (Fin N → ℝ))46 (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :47 (Fin n → ℝ) → (Fin N → ℝ) :=48 fun x => Classical.choose ((lipschitzOnWith_modelBoundaryAmbient M g hg).extend_pi)49 (show Space M from x)5051private theorem modelMcShaneToCoord_spec {n N : ℕ}52 (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ))53 (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :54 (∀ x y, ‖modelMcShaneToCoord M g hg x - modelMcShaneToCoord M g hg y‖ ≤55 M.p (x - y)) ∧ (∀ u : M.unitSphere, modelMcShaneToCoord M g hg u = g u) := by56 have hs := Classical.choose_spec ((lipschitzOnWith_modelBoundaryAmbient M g hg).extend_pi)57 constructor58 · intro x y59 have h := hs.1.dist_le_mul (show Space M from x) (show Space M from y)60 simpa only [modelMcShaneToCoord, NNReal.coe_one, one_mul, dist_eq_norm,61 norm_space_eq, toReference_sub_ofReference]62 using h63 · intro u64 have hu' : M.p u.val = 1 := u.property65 have hu : (show Space M from u.val) ∈ Metric.sphere (0 : Space M) 1 :=66 mem_sphere_zero_iff_norm.mpr u.property67 simpa [modelMcShaneToCoord, modelBoundaryAmbient, hu'] using (hs.2 hu).symm6869private structure BoundaryExtensionData {n N : ℕ}70 (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ)) where71 toFun : (Fin n → ℝ) → (Fin N → ℝ)72 norm_sub_le_seminorm_sub : ∀ x y, ‖toFun x - toFun y‖ ≤ M.p (x - y)73 apply_coe_unitSphere : ∀ u : M.unitSphere, toFun (u : Fin n → ℝ) = g u74 ae_isContraction_fderiv :75 ∀ᵐ x ∂volume.restrict M.closedUnitBall, M.IsContraction (fderiv ℝ toFun x)76 integrableOn_derivativeGenerator :77 IntegrableOn (derivativeGenerator M toFun) M.closedUnitBall volume78 average_mem : derivativeAverage M toFun ∈ PluckerBody.body M N7980private def concreteBoundaryExtensionData {n N : ℕ}81 (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ))82 (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :83 BoundaryExtensionData M g := by84 have h := modelMcShaneToCoord_spec M g hg85 have hc : ∀ᵐ x ∂volume.restrict M.closedUnitBall,86 M.IsContraction (fderiv ℝ (modelMcShaneToCoord M g hg) x) :=87 FDeriv.ae_norm_apply_le_seminorm_of_lipschitz M.p88 ⟨M.upper, M.upper_pos.le⟩ M.le_upper h.1 M.closedUnitBall89 have hi := integrableOn_derivativeGenerator_of_seminormLipschitz M h.190 exact ⟨modelMcShaneToCoord M g hg, h.1, h.2, hc, hi,91 derivativeAverage_mem_body M hc hi⟩9293end Internal9495/-- Every seminorm-Lipschitz boundary map has an extension with its prescribed96trace, almost everywhere contractive derivative, integrable derivative97generator, and derivative average in the Plücker body. -/98theorem exists_extension_with_derivativeAverage_mem {n N : ℕ}99 (M : EquivalentSeminorm (Fin n → ℝ)) (g : M.unitSphere → (Fin N → ℝ))100 (hg : ∀ u v, ‖g u - g v‖ ≤ M.p ((u : Fin n → ℝ) - (v : Fin n → ℝ))) :101 ∃ f : (Fin n → ℝ) → (Fin N → ℝ),102 (∀ x y, ‖f x - f y‖ ≤ M.p (x - y)) ∧103 (∀ u : M.unitSphere, f u = g u) ∧104 (∀ᵐ x ∂volume.restrict M.closedUnitBall, M.IsContraction (fderiv ℝ f x)) ∧105 IntegrableOn (derivativeGenerator M f) M.closedUnitBall volume ∧106 derivativeAverage M f ∈ PluckerBody.body M N := by107 let d := Internal.concreteBoundaryExtensionData M g hg108 exact ⟨d.toFun, d.norm_sub_le_seminorm_sub, d.apply_coe_unitSphere, d.ae_isContraction_fderiv,109 d.integrableOn_derivativeGenerator, d.average_mem⟩110111namespace Internal112113private def coordinateBoundaryData {m N : ℕ}114 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}115 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1)116 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) : MX.unitSphere → (Fin N → ℝ) :=117 fun u => A (show Fin (m + 1) → ℝ from118 (Δ ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩).val)119120private theorem norm_coordinateBoundaryData_sub_le_seminorm_sub {m N : ℕ}121 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}122 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1)123 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) (hA : MY.IsContraction A) :124 ∀ u v, ‖coordinateBoundaryData Δ A u - coordinateBoundaryData Δ A v‖ ≤125 MX.p ((u : Fin (m + 1) → ℝ) - (v : Fin (m + 1) → ℝ)) := by126 intro u v127 let u' : Metric.sphere (0 : Space MX) 1 :=128 ⟨(show Space MX from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩129 let v' : Metric.sphere (0 : Space MX) 1 :=130 ⟨(show Space MX from v.val), mem_sphere_zero_iff_norm.mpr v.property⟩131 have chord : MY.p ((show Fin (m + 1) → ℝ from (Δ u').val) -132 (show Fin (m + 1) → ℝ from (Δ v').val)) = MX.p (u.val - v.val) := by133 simpa only [Subtype.dist_eq, dist_space_eq] using Δ.isometry.dist_eq u' v'134 calc135 ‖coordinateBoundaryData Δ A u - coordinateBoundaryData Δ A v‖ =136 ‖A ((show Fin (m + 1) → ℝ from (Δ u').val) -137 (show Fin (m + 1) → ℝ from (Δ v').val))‖ := by138 simp [coordinateBoundaryData, u', v', map_sub]139 _ ≤ MY.p ((show Fin (m + 1) → ℝ from (Δ u').val) -140 (show Fin (m + 1) → ℝ from (Δ v').val)) := hA _141 _ = MX.p (u.val - v.val) := chord142143private def boundaryExtensionData {m N : ℕ}144 {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}145 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1)146 (A : (Fin (m + 1) → ℝ) →L[ℝ] (Fin N → ℝ)) (hA : MY.IsContraction A) :147 BoundaryExtensionData MX (coordinateBoundaryData Δ A) :=148 concreteBoundaryExtensionData MX (coordinateBoundaryData Δ A)149 (norm_coordinateBoundaryData_sub_le_seminorm_sub Δ A hA)150151end Internal152end MathlibAnnex.Plucker