Exact source: MathlibAnnex/Analysis/Normed/Sphere/RadialBall.lean
Pinned GitHub source · Raw UTF-8 source
Back to The absolute Jacobian integral of a radial sphere extension
1import MathlibAnnex.Analysis.Normed.Sphere.RadialExtension2import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport34/-! # Radial image of equivalent seminorm unit balls5The model norm lives on `Space M`; the underlying finite Pi carrier retains its6reference norm. All radial maps below use the accepted radialExtension exactly.7No positive-dimension hypothesis is needed for the ball image or distance bounds.8-/910noncomputable section11open Set Metric Function12open scoped NNReal ENNReal13namespace MathlibAnnex.Sphere14open EquivalentSeminorm1516private abbrev radialMap {n : ℕ}17 {MX MY : EquivalentSeminorm (Fin n → ℝ)}18 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1)19 (x : Fin n → ℝ) : Fin n → ℝ :=20 show Fin n → ℝ from radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x)2122@[simp] private theorem radialMap_p {n : ℕ}23 {MX MY : EquivalentSeminorm (Fin n → ℝ)}24 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x : Fin n → ℝ) :25 MY.p (radialMap Δ x) = MX.p x := radialExtension_norm Δ (show Space MX from x)2627private theorem radialMap_leftInverse {n : ℕ}28 {MX MY : EquivalentSeminorm (Fin n → ℝ)}29 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :30 LeftInverse (radialMap Δ.symm) (radialMap Δ) :=31 fun x => radialExtension_leftInverse Δ (show Space MX from x)3233private theorem radialMap_model_dist {n : ℕ}34 {MX MY : EquivalentSeminorm (Fin n → ℝ)}35 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :36 MY.p (radialMap Δ x - radialMap Δ y) ≤ 3 * MX.p (x - y) := by37 have h := (lipschitzWith_radialExtension Δ).dist_le_mul38 (show Space MX from x) (show Space MX from y)39 simpa only [dist_space_eq, NNReal.coe_ofNat] using h4041private theorem lipschitzWith_radialMap {n : ℕ}42 {MX MY : EquivalentSeminorm (Fin n → ℝ)}43 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :44 LipschitzWith (3 * MX.upper / MY.lower).toNNReal (radialMap Δ) := by45 have hC : 0 ≤ 3 * MX.upper / MY.lower := div_nonneg (mul_nonneg (by norm_num) MX.upper_pos.le) MY.lower_pos.le46 refine LipschitzWith.of_dist_le_mul ?_47 intro x y48 have hlower := MY.lower_le (radialMap Δ x - radialMap Δ y)49 have hmodel := radialMap_model_dist Δ x y50 have hupper := MX.le_upper (x - y)51 rw [Real.coe_toNNReal _ hC, dist_eq_norm, dist_eq_norm]52 calc53 ‖radialMap Δ x - radialMap Δ y‖ ≤ (3 * MX.upper * ‖x - y‖) / MY.lower :=54 (le_div_iff₀ MY.lower_pos).2 (by nlinarith)55 _ = (3 * MX.upper / MY.lower) * ‖x - y‖ := by ring5657namespace Internal58private def modelRadialAntiConstant {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) : ℝ :=59 MX.lower / (3 * MY.upper)6061private theorem modelRadialAntiConstant_pos {n : ℕ} (MX MY : EquivalentSeminorm (Fin n → ℝ)) :62 0 < modelRadialAntiConstant MX MY :=63 div_pos MX.lower_pos (mul_pos (by norm_num) MY.upper_pos)64end Internal65open Internal6667private theorem radialMap_lower {n : ℕ}68 {MX MY : EquivalentSeminorm (Fin n → ℝ)}69 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) (x y : Fin n → ℝ) :70 modelRadialAntiConstant MX MY * ‖x - y‖ ≤ ‖radialMap Δ x - radialMap Δ y‖ := by71 have hinv := radialMap_model_dist Δ.symm (radialMap Δ x) (radialMap Δ y)72 rw [radialMap_leftInverse Δ x, radialMap_leftInverse Δ y] at hinv73 have hlow := MX.lower_le (x - y)74 have hup := MY.le_upper (radialMap Δ x - radialMap Δ y)75 have hden : 0 < 3 * MY.upper := mul_pos (by norm_num) MY.upper_pos76 have hprod : MX.lower * ‖x - y‖ ≤ (3 * MY.upper) *77 ‖radialMap Δ x - radialMap Δ y‖ := by nlinarith78 dsimp [modelRadialAntiConstant]79 calc80 MX.lower / (3 * MY.upper) * ‖x - y‖ =81 (MX.lower * ‖x - y‖) / (3 * MY.upper) := by ring82 _ ≤ ‖radialMap Δ x - radialMap Δ y‖ :=83 (div_le_iff₀ hden).2 (by simpa only [mul_comm] using hprod)8485private theorem isOpen_seminorm_ball {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :86 IsOpen (M.p.ball 0 1) := by87 rw [Seminorm.ball_zero_eq]88 exact isOpen_lt M.continuous_p continuous_const8990private theorem convex_seminorm_ball {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :91 Convex ℝ (M.p.ball 0 1) := M.p.convex_ball 0 19293private theorem isConnected_seminorm_ball {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :94 IsConnected (M.p.ball 0 1) := by95 refine (convex_seminorm_ball M).isConnected ?_96 exact ⟨0, by simp⟩9798namespace Internal99100/-- Identity equivalence between the metric sphere of the model copy and its101seminorm level set on reference coordinates. -/102private def modelSphereCopyEquiv {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :103 sphere (0 : Space M) 1 ≃ M.unitSphere where104 toFun u := ⟨(show Fin n → ℝ from u.val), sphere_apply M u⟩105 invFun u := ⟨(show Space M from u.val), mem_sphere_zero_iff_norm.mpr u.property⟩106 left_inv u := by cases u; rfl107 right_inv u := by cases u; rfl108109/-- Under the frozen ModelSphereIso substitution the ordinary sphere isometry110is already the input; transport is the identity. -/111private def modelSphereIsoToSphereIso {n : ℕ}112 {MX MY : EquivalentSeminorm (Fin n → ℝ)}113 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :114 sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1 := Δ115116@[simp] private theorem modelSphereIsoToSphereIso_symm {n : ℕ}117 {MX MY : EquivalentSeminorm (Fin n → ℝ)}118 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :119 modelSphereIsoToSphereIso Δ.symm = (modelSphereIsoToSphereIso Δ).symm := rfl120121private theorem antilipschitzWith_radialMap {n : ℕ}122 {MX MY : EquivalentSeminorm (Fin n → ℝ)}123 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :124 AntilipschitzWith (modelRadialAntiConstant MX MY).toNNReal⁻¹ (radialMap Δ) := by125 refine AntilipschitzWith.of_le_mul_dist ?_126 intro x y127 have h := radialMap_lower Δ x y128 have hc := modelRadialAntiConstant_pos MX MY129 have h' : ‖x - y‖ ≤ (modelRadialAntiConstant MX MY)⁻¹ *130 ‖radialMap Δ x - radialMap Δ y‖ := by131 rw [inv_mul_eq_div]132 exact (le_div_iff₀ hc).2 (by simpa only [mul_comm] using h)133 simpa only [dist_eq_norm, NNReal.coe_inv,134 Real.coe_toNNReal (modelRadialAntiConstant MX MY) hc.le] using h'135end Internal136137/-- The accepted radial extension in reference coordinates maps the source open138unit seminorm ball exactly onto the target open unit seminorm ball. -/139theorem radialExtension_image_ball {n : ℕ}140 {MX MY : EquivalentSeminorm (Fin n → ℝ)}141 (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :142 (fun x : Fin n → ℝ => (show Fin n → ℝ from143 radialExtension (X := Space MX) (Y := Space MY) Δ (show Space MX from x))) '' MX.p.ball 0 1 = MY.p.ball 0 1 := by144 change radialMap Δ '' MX.p.ball 0 1 = MY.p.ball 0 1145 simp only [Seminorm.ball_zero_eq]146 ext y147 constructor148 · rintro ⟨x, hx, rfl⟩149 simpa only [mem_setOf_eq, radialMap_p] using hx150 · intro hy151 refine ⟨radialMap Δ.symm y, ?_, ?_⟩152 · simpa only [mem_setOf_eq, radialMap_p] using hy153 · exact radialMap_leftInverse Δ.symm y154155private theorem setOf_seminorm_lt_one_eq_ball {n : ℕ} (M : EquivalentSeminorm (Fin n → ℝ)) :156 {x | M.p x < 1} = M.p.ball 0 1 := (Seminorm.ball_zero_eq M.p).symm157158end MathlibAnnex.Sphere