Exact source: MathlibAnnex/Analysis/Normed/Ball/VolumeRigidity.lean
Pinned GitHub source · Raw UTF-8 source
Back to All Plücker bodies determine the norm up to linear isometry
1import Mathlib.Analysis.Seminorm2import Mathlib.Analysis.Normed.Module.FiniteDimension3import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar4import Mathlib.MeasureTheory.Measure.OpenPos56/-!7# Strict volume and gauge rigidity for unit balls89This candidate separates two reusable facts.1011* A compact proper subset of the closed unit ball of a continuous real seminorm leaves an open12 defect and therefore has strictly smaller additive Haar measure.13* Inclusion, respectively equality, of closed seminorm unit balls under a linear map gives a14 pointwise seminorm inequality, respectively equality.1516No convexity of the compact subset is assumed. Equality of measures is never used without an17independent set-inclusion hypothesis.1819This file is a build candidate. It becomes an admitted MathlibAnnex source only after the pinned20local integration build, recovery tests, dependency audit, and owner-authorized admission.21-/2223noncomputable section2425open Set MeasureTheory26open scoped ENNReal2728namespace MathlibAnnex2930namespace SeminormBall3132variable {E F : Type*}3334private theorem mem_interior_of_lt35 [NormedAddCommGroup E] [NormedSpace ℝ E]36 (p : Seminorm ℝ E) (hp : Continuous p) {x : E} (hx : p x < 1) :37 x ∈ interior (p.closedBall 0 1) := by38 have hopen : IsOpen {z : E | p z < 1} :=39 isOpen_lt hp continuous_const40 have hsub : {z : E | p z < 1} ⊆ p.closedBall 0 1 := by41 intro z hz42 exact p.mem_closedBall_zero.mpr hz.le43 exact interior_maximal hsub hopen hx4445private theorem exists_radial_contraction46 [NormedAddCommGroup E] [NormedSpace ℝ E]47 {K : Set E} (hK : IsClosed K) {y : E} (hy : y ∉ K) :48 ∃ t : ℝ, 0 < t ∧ t < 1 ∧ t • y ∉ K := by49 have hopen : IsOpen Kᶜ := hK.isOpen_compl50 rcases (Metric.isOpen_iff.mp hopen y hy) with ⟨δ, hδ, hball⟩51 let a : ℝ := min (1 / 2 : ℝ) (δ / (2 * (‖y‖ + 1)))52 have ha : 0 < a := by53 dsimp [a]54 positivity55 have ha_half : a ≤ (1 / 2 : ℝ) := min_le_left _ _56 have ha_delta : a ≤ δ / (2 * (‖y‖ + 1)) := min_le_right _ _57 let t : ℝ := 1 - a58 have ht0 : 0 < t := by59 dsimp [t]60 linarith61 have ht1 : t < 1 := by62 dsimp [t]63 linarith64 have ht_sub : t - 1 = -a := by simp [t]65 have habs : |t - 1| = a := by66 rw [ht_sub, abs_neg, abs_of_pos ha]67 have hdist : dist (t • y) y < δ := by68 rw [dist_eq_norm]69 have hsubsmul : t • y - y = (t - 1) • y := by module70 rw [hsubsmul, norm_smul, Real.norm_eq_abs, habs]71 have hnorm : ‖y‖ < ‖y‖ + 1 := by linarith [norm_nonneg y]72 calc73 a * ‖y‖ ≤ (δ / (2 * (‖y‖ + 1))) * ‖y‖ :=74 mul_le_mul_of_nonneg_right ha_delta (norm_nonneg y)75 _ < (δ / (2 * (‖y‖ + 1))) * (‖y‖ + 1) := by76 gcongr77 _ = δ / 2 := by78 field_simp [show 0 < ‖y‖ + 1 by positivity]79 _ < δ := by linarith80 have hmem : t • y ∈ Metric.ball y δ := by81 simpa [Metric.mem_ball] using hdist82 exact ⟨t, ht0, ht1, hball hmem⟩8384/-- A compact proper subset of the closed unit ball of a continuous real seminorm leaves a85nonempty open defect. The compact set itself need not be convex. -/86theorem interior_sdiff_nonempty87 [NormedAddCommGroup E] [NormedSpace ℝ E]88 (p : Seminorm ℝ E) (hp : Continuous p)89 {K : Set E} (hKcompact : IsCompact K)90 (hsub : K ⊆ p.closedBall 0 1) (hne : K ≠ p.closedBall 0 1) :91 (interior (p.closedBall 0 1 \ K)).Nonempty := by92 have hproper : ∃ y, y ∈ p.closedBall 0 1 ∧ y ∉ K := by93 by_contra h94 push Not at h95 exact hne (Set.Subset.antisymm hsub h)96 rcases hproper with ⟨y, hyBall, hyK⟩97 rcases exists_radial_contraction hKcompact.isClosed hyK with98 ⟨t, ht0, ht1, htyK⟩99 have htyInt : t • y ∈ interior (p.closedBall 0 1) := by100 apply mem_interior_of_lt p hp101 rw [map_smul_eq_mul p t y, Real.norm_eq_abs, abs_of_pos ht0]102 have hpy : p y ≤ 1 := p.mem_closedBall_zero.mp hyBall103 calc104 t * p y ≤ t * 1 := mul_le_mul_of_nonneg_left hpy ht0.le105 _ = t := by ring106 _ < 1 := ht1107 have hopen : IsOpen (interior (p.closedBall 0 1) ∩ Kᶜ) :=108 isOpen_interior.inter hKcompact.isClosed.isOpen_compl109 have hsubset : interior (p.closedBall 0 1) ∩ Kᶜ ⊆110 p.closedBall 0 1 \ K := by111 intro z hz112 exact ⟨interior_subset hz.1, hz.2⟩113 have hinter : interior (p.closedBall 0 1) ∩ Kᶜ ⊆114 interior (p.closedBall 0 1 \ K) :=115 interior_maximal hsubset hopen116 exact ⟨t • y, hinter ⟨htyInt, htyK⟩⟩117118/-- A compact proper subset of the closed unit ball of a continuous real seminorm has strictly119smaller additive Haar measure. -/120theorem measure_lt121 [NormedAddCommGroup E] [NormedSpace ℝ E]122 [MeasurableSpace E] [BorelSpace E]123 (μ : Measure E) [Measure.IsAddHaarMeasure μ]124 (p : Seminorm ℝ E) (hp : Continuous p)125 {K : Set E} (hKcompact : IsCompact K)126 (hsub : K ⊆ p.closedBall 0 1) (hne : K ≠ p.closedBall 0 1) :127 μ K < μ (p.closedBall 0 1) := by128 have hdiff_nonzero : μ (p.closedBall 0 1 \ K) ≠ 0 :=129 (Measure.measure_pos_of_nonempty_interior μ130 (interior_sdiff_nonempty p hp hKcompact hsub hne)).ne'131 have hKmeas : MeasurableSet K := hKcompact.measurableSet132 have hballClosed : IsClosed (p.closedBall 0 1) := by133 rw [show p.closedBall 0 1 = {x : E | p x ≤ 1} by134 ext x135 exact p.mem_closedBall_zero]136 exact isClosed_le hp continuous_const137 have hdecomp : p.closedBall 0 1 = K ∪ (p.closedBall 0 1 \ K) := by138 ext x139 constructor140 · intro hx141 by_cases hxK : x ∈ K142 · exact Or.inl hxK143 · exact Or.inr ⟨hx, hxK⟩144 · intro hx145 exact hx.elim (fun hxK => hsub hxK) (fun h => h.1)146 have hdiffmeas : MeasurableSet (p.closedBall 0 1 \ K) :=147 hballClosed.measurableSet.diff hKmeas148 rw [hdecomp, measure_union disjoint_sdiff_right hdiffmeas]149 exact ENNReal.lt_add_right hKcompact.measure_ne_top hdiff_nonzero150151/-- Inclusion of closed seminorm unit balls gives the pointwise gauge inequality. -/152theorem map_le153 [AddCommGroup E] [Module ℝ E]154 [AddCommGroup F] [Module ℝ F]155 (p : Seminorm ℝ E) (q : Seminorm ℝ F)156 (hp : ∀ x : E, p x = 0 → x = 0)157 (L : E →ₗ[ℝ] F)158 (hsub : L '' p.closedBall 0 1 ⊆ q.closedBall 0 1) (x : E) :159 q (L x) ≤ p x := by160 by_cases hx : x = 0161 · subst x162 simp163 let a : ℝ := p x164 have ha_nonneg : 0 ≤ p x := apply_nonneg p x165 have ha_ne : p x ≠ 0 := fun h => hx (hp x h)166 have ha : 0 < a := by167 dsimp [a]168 exact lt_of_le_of_ne ha_nonneg ha_ne.symm169 have hu : a⁻¹ • x ∈ p.closedBall 0 1 := by170 apply p.mem_closedBall_zero.mpr171 rw [map_smul_eq_mul p a⁻¹ x, Real.norm_eq_abs,172 abs_of_pos (inv_pos.mpr ha)]173 simp [a, ha.ne']174 have hLu : L (a⁻¹ • x) ∈ q.closedBall 0 1 := hsub ⟨_, hu, rfl⟩175 have hscaled : a⁻¹ * q (L x) ≤ 1 := by176 simpa [map_smul, map_smul_eq_mul q, Real.norm_eq_abs,177 abs_of_pos ha] using q.mem_closedBall_zero.mp hLu178 have hdiv : q (L x) / a ≤ 1 := by179 simpa [div_eq_inv_mul, mul_comm] using hscaled180 have hle : q (L x) ≤ 1 * a := (div_le_iff₀ ha).mp hdiv181 simpa [a] using hle182183/-- A bijective linear map carrying one closed seminorm unit ball exactly onto another preserves184both gauges. -/185theorem map_eq186 [AddCommGroup E] [Module ℝ E]187 [AddCommGroup F] [Module ℝ F]188 (p : Seminorm ℝ E) (q : Seminorm ℝ F)189 (hp : ∀ x : E, p x = 0 → x = 0)190 (hq : ∀ y : F, q y = 0 → y = 0)191 (L : E →ₗ[ℝ] F) (hbij : Function.Bijective L)192 (hball : L '' p.closedBall 0 1 = q.closedBall 0 1) (x : E) :193 q (L x) = p x := by194 let e : E ≃ₗ[ℝ] F := LinearEquiv.ofBijective L hbij195 have hforwardSubset : L '' p.closedBall 0 1 ⊆ q.closedBall 0 1 := by196 intro y hy197 rwa [← hball]198 have hforward : q (L x) ≤ p x :=199 map_le p q hp L hforwardSubset x200 have hinverse : e.symm '' q.closedBall 0 1 ⊆ p.closedBall 0 1 := by201 intro z hz202 rcases hz with ⟨y, hy, rfl⟩203 rw [← hball] at hy204 rcases hy with ⟨u, hu, hLu⟩205 have hEq : e.symm y = u := by206 apply e.injective207 simp [e, hLu]208 simpa [hEq] using hu209 have hreverse : p (e.symm (L x)) ≤ q (L x) :=210 map_le q p hq e.symm.toLinearMap hinverse (L x)211 have hEx : e.symm (L x) = x := by simp [e]212 exact le_antisymm hforward (by simpa [hEx] using hreverse)213214end SeminormBall215216namespace NormBall217218variable {E F : Type*}219220/-- Standard-norm specialization of `SeminormBall.measure_lt`. -/221theorem measure_lt222 [NormedAddCommGroup E] [NormedSpace ℝ E]223 [MeasurableSpace E] [BorelSpace E]224 (μ : Measure E) [Measure.IsAddHaarMeasure μ]225 {K : Set E} (hKcompact : IsCompact K)226 (hsub : K ⊆ Metric.closedBall (0 : E) 1)227 (hne : K ≠ Metric.closedBall (0 : E) 1) :228 μ K < μ (Metric.closedBall (0 : E) 1) := by229 let p : Seminorm ℝ E := normSeminorm ℝ E230 have hp : Continuous p := by231 simpa [p] using (continuous_norm : Continuous fun x : E => ‖x‖)232 have hsub' : K ⊆ p.closedBall 0 1 := by233 simpa [p] using hsub234 have hne' : K ≠ p.closedBall 0 1 := by235 simpa [p] using hne236 simpa [p] using237 (SeminormBall.measure_lt μ p hp hKcompact hsub' hne')238239/-- Standard-norm specialization of `SeminormBall.map_le`. -/240theorem map_le241 [NormedAddCommGroup E] [NormedSpace ℝ E]242 [NormedAddCommGroup F] [NormedSpace ℝ F]243 (L : E →ₗ[ℝ] F)244 (hsub : L '' Metric.closedBall (0 : E) 1 ⊆245 Metric.closedBall (0 : F) 1) (x : E) :246 ‖L x‖ ≤ ‖x‖ := by247 let p : Seminorm ℝ E := normSeminorm ℝ E248 let q : Seminorm ℝ F := normSeminorm ℝ F249 have hp : ∀ z : E, p z = 0 → z = 0 := by250 intro z hz251 exact norm_eq_zero.mp (by simpa [p] using hz)252 have hsub' : L '' p.closedBall 0 1 ⊆ q.closedBall 0 1 := by253 simpa [p, q] using hsub254 simpa [p, q] using255 (SeminormBall.map_le p q hp L hsub' x)256257/-- Standard-norm specialization of `SeminormBall.map_eq`. -/258theorem map_eq259 [NormedAddCommGroup E] [NormedSpace ℝ E]260 [NormedAddCommGroup F] [NormedSpace ℝ F]261 (L : E →ₗ[ℝ] F) (hbij : Function.Bijective L)262 (hball : L '' Metric.closedBall (0 : E) 1 =263 Metric.closedBall (0 : F) 1) (x : E) :264 ‖L x‖ = ‖x‖ := by265 let p : Seminorm ℝ E := normSeminorm ℝ E266 let q : Seminorm ℝ F := normSeminorm ℝ F267 have hp : ∀ z : E, p z = 0 → z = 0 := by268 intro z hz269 exact norm_eq_zero.mp (by simpa [p] using hz)270 have hq : ∀ z : F, q z = 0 → z = 0 := by271 intro z hz272 exact norm_eq_zero.mp (by simpa [q] using hz)273 have hball' : L '' p.closedBall 0 1 = q.closedBall 0 1 := by274 simpa [p, q] using hball275 simpa [p, q] using276 (SeminormBall.map_eq p q hp hq L hbij hball' x)277278end NormBall279280end MathlibAnnex