Skip to content

Commit 7a30096

Browse files
Parcly-TaxelParcly-Taxel
committed
feat: port Analysis.NormedSpace.AddTorsor (#3477)
1 parent fda02e8 commit 7a30096

File tree

3 files changed

+215
-4
lines changed

3 files changed

+215
-4
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -328,6 +328,7 @@ import Mathlib.Analysis.Normed.Order.Basic
328328
import Mathlib.Analysis.Normed.Order.Lattice
329329
import Mathlib.Analysis.Normed.Order.UpperLower
330330
import Mathlib.Analysis.Normed.Ring.Seminorm
331+
import Mathlib.Analysis.NormedSpace.AddTorsor
331332
import Mathlib.Analysis.NormedSpace.Basic
332333
import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
333334
import Mathlib.Analysis.NormedSpace.Extr

‎Mathlib/Analysis/NormedSpace/AddTorsor.lean‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
/-
2+
Copyright (c) 2020 Joseph Myers. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joseph Myers, Yury Kudryashov
5+
6+
! This file was ported from Lean 3 source module analysis.normed_space.add_torsor
7+
! leanprover-community/mathlib commit 78261225eb5cedc61c5c74ecb44e5b385d13b733
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Analysis.NormedSpace.Basic
12+
import Mathlib.Analysis.Normed.Group.AddTorsor
13+
import Mathlib.LinearAlgebra.AffineSpace.MidpointZero
14+
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
15+
import Mathlib.Topology.Instances.RealVectorSpace
16+
17+
/-!
18+
# Torsors of normed space actions.
19+
20+
This file contains lemmas about normed additive torsors over normed spaces.
21+
-/
22+
23+
24+
noncomputable section
25+
26+
open NNReal Topology
27+
28+
open Filter
29+
30+
variable {α V P W Q : Type _} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P]
31+
[NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q]
32+
33+
section NormedSpace
34+
35+
variable {𝕜 : Type _} [NormedField 𝕜] [NormedSpace 𝕜 V] [NormedSpace 𝕜 W]
36+
37+
open AffineMap
38+
39+
theorem AffineSubspace.isClosed_direction_iff (s : AffineSubspace 𝕜 Q) :
40+
IsClosed (s.direction : Set W) ↔ IsClosed (s : Set Q) := by
41+
rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩); · simp [isClosed_singleton]
42+
rw [← (IsometryEquiv.vaddConst x).toHomeomorph.symm.isClosed_image,
43+
AffineSubspace.coe_direction_eq_vsub_set_right hx]
44+
rfl
45+
#align affine_subspace.is_closed_direction_iff AffineSubspace.isClosed_direction_iff
46+
47+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
48+
@[simp]
49+
theorem dist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
50+
dist p₁ (homothety p₁ c p₂) = ‖c‖ * dist p₁ p₂ := by
51+
-- Porting note: was `simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]`
52+
rw [homothety_def, dist_eq_norm_vsub V]
53+
simp [norm_smul, ← dist_eq_norm_vsub V, dist_comm]
54+
#align dist_center_homothety dist_center_homothety
55+
56+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
57+
@[simp]
58+
theorem dist_homothety_center (p₁ p₂ : P) (c : 𝕜) :
59+
dist (homothety p₁ c p₂) p₁ = ‖c‖ * dist p₁ p₂ := by rw [dist_comm, dist_center_homothety]
60+
#align dist_homothety_center dist_homothety_center
61+
62+
@[simp]
63+
theorem dist_lineMap_lineMap (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
64+
dist (lineMap p₁ p₂ c₁) (lineMap p₁ p₂ c₂) = dist c₁ c₂ * dist p₁ p₂ := by
65+
rw [dist_comm p₁ p₂]
66+
-- Porting note: was `simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,`
67+
-- `← sub_smul, norm_smul, vsub_eq_sub]`
68+
rw [lineMap_apply, lineMap_apply, dist_eq_norm_vsub V, vadd_vsub_vadd_cancel_right,
69+
← sub_smul, norm_smul, ← vsub_eq_sub, ← dist_eq_norm_vsub V, ← dist_eq_norm_vsub 𝕜]
70+
#align dist_line_map_line_map dist_lineMap_lineMap
71+
72+
theorem lipschitzWith_lineMap (p₁ p₂ : P) : LipschitzWith (nndist p₁ p₂) (lineMap p₁ p₂ : 𝕜 → P) :=
73+
LipschitzWith.of_dist_le_mul fun c₁ c₂ =>
74+
((dist_lineMap_lineMap p₁ p₂ c₁ c₂).trans (mul_comm _ _)).le
75+
#align lipschitz_with_line_map lipschitzWith_lineMap
76+
77+
@[simp]
78+
theorem dist_lineMap_left (p₁ p₂ : P) (c : 𝕜) : dist (lineMap p₁ p₂ c) p₁ = ‖c‖ * dist p₁ p₂ := by
79+
-- Porting note: was
80+
-- simpa only [lineMap_apply_zero, dist_zero_right] using dist_lineMap_lineMap p₁ p₂ c 0
81+
rw [← dist_zero_right, ← dist_lineMap_lineMap, lineMap_apply_zero]
82+
#align dist_line_map_left dist_lineMap_left
83+
84+
@[simp]
85+
theorem dist_left_lineMap (p₁ p₂ : P) (c : 𝕜) : dist p₁ (lineMap p₁ p₂ c) = ‖c‖ * dist p₁ p₂ :=
86+
(dist_comm _ _).trans (dist_lineMap_left _ _ _)
87+
#align dist_left_line_map dist_left_lineMap
88+
89+
@[simp]
90+
theorem dist_lineMap_right (p₁ p₂ : P) (c : 𝕜) :
91+
dist (lineMap p₁ p₂ c) p₂ = ‖1 - c‖ * dist p₁ p₂ := by
92+
-- Porting note: was
93+
-- `simpa only [lineMap_apply_one, dist_eq_norm'] using dist_lineMap_lineMap p₁ p₂ c 1`
94+
rw [← dist_eq_norm', ← dist_lineMap_lineMap, lineMap_apply_one]
95+
#align dist_line_map_right dist_lineMap_right
96+
97+
@[simp]
98+
theorem dist_right_lineMap (p₁ p₂ : P) (c : 𝕜) : dist p₂ (lineMap p₁ p₂ c) = ‖1 - c‖ * dist p₁ p₂ :=
99+
(dist_comm _ _).trans (dist_lineMap_right _ _ _)
100+
#align dist_right_line_map dist_right_lineMap
101+
102+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
103+
@[simp]
104+
theorem dist_homothety_self (p₁ p₂ : P) (c : 𝕜) :
105+
dist (homothety p₁ c p₂) p₂ = ‖1 - c‖ * dist p₁ p₂ := by
106+
rw [homothety_eq_lineMap, dist_lineMap_right]
107+
#align dist_homothety_self dist_homothety_self
108+
109+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
110+
@[simp]
111+
theorem dist_self_homothety (p₁ p₂ : P) (c : 𝕜) :
112+
dist p₂ (homothety p₁ c p₂) = ‖1 - c‖ * dist p₁ p₂ := by rw [dist_comm, dist_homothety_self]
113+
#align dist_self_homothety dist_self_homothety
114+
115+
section invertibleTwo
116+
117+
variable [Invertible (2 : 𝕜)]
118+
119+
@[simp]
120+
theorem dist_left_midpoint (p₁ p₂ : P) : dist p₁ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
121+
rw [midpoint, dist_comm, dist_lineMap_left, invOf_eq_inv, ← norm_inv]
122+
#align dist_left_midpoint dist_left_midpoint
123+
124+
@[simp]
125+
theorem dist_midpoint_left (p₁ p₂ : P) : dist (midpoint 𝕜 p₁ p₂) p₁ = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
126+
rw [dist_comm, dist_left_midpoint]
127+
#align dist_midpoint_left dist_midpoint_left
128+
129+
@[simp]
130+
theorem dist_midpoint_right (p₁ p₂ : P) :
131+
dist (midpoint 𝕜 p₁ p₂) p₂ = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
132+
rw [midpoint_comm, dist_midpoint_left, dist_comm]
133+
#align dist_midpoint_right dist_midpoint_right
134+
135+
@[simp]
136+
theorem dist_right_midpoint (p₁ p₂ : P) :
137+
dist p₂ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂ := by
138+
rw [dist_comm, dist_midpoint_right]
139+
#align dist_right_midpoint dist_right_midpoint
140+
141+
theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) :
142+
dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖(2 : 𝕜)‖ := by
143+
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint]
144+
try infer_instance
145+
rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul]
146+
exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _)
147+
#align dist_midpoint_midpoint_le' dist_midpoint_midpoint_le'
148+
149+
end invertibleTwo
150+
151+
theorem antilipschitzWith_lineMap {p₁ p₂ : Q} (h : p₁ ≠ p₂) :
152+
AntilipschitzWith (nndist p₁ p₂)⁻¹ (lineMap p₁ p₂ : 𝕜 → Q) :=
153+
AntilipschitzWith.of_le_mul_dist fun c₁ c₂ => by
154+
rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
155+
inv_mul_cancel (dist_ne_zero.2 h), mul_one]
156+
#align antilipschitz_with_line_map antilipschitzWith_lineMap
157+
158+
variable (𝕜)
159+
160+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
161+
theorem eventually_homothety_mem_of_mem_interior (x : Q) {s : Set Q} {y : Q} (hy : y ∈ interior s) :
162+
∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s := by
163+
rw [(NormedAddCommGroup.nhds_basis_norm_lt (1 : 𝕜)).eventually_iff]
164+
cases' eq_or_ne y x with h h
165+
· use 1
166+
simp [h.symm, interior_subset hy]
167+
have hxy : 0 < ‖y -ᵥ x‖ := by rwa [norm_pos_iff, vsub_ne_zero]
168+
obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy
169+
obtain ⟨ε, hε, hyε⟩ := Metric.isOpen_iff.mp hu₂ y hu₃
170+
refine' ⟨ε / ‖y -ᵥ x‖, div_pos hε hxy, fun δ (hδ : ‖δ - 1‖ < ε / ‖y -ᵥ x‖) => hu₁ (hyε _)⟩
171+
rw [lt_div_iff hxy, ← norm_smul, sub_smul, one_smul] at hδ
172+
rwa [homothety_apply, Metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub]
173+
#align eventually_homothety_mem_of_mem_interior eventually_homothety_mem_of_mem_interior
174+
175+
set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
176+
theorem eventually_homothety_image_subset_of_finite_subset_interior (x : Q) {s : Set Q} {t : Set Q}
177+
(ht : t.Finite) (h : t ⊆ interior s) : ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ '' t ⊆ s := by
178+
suffices ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s by
179+
simp_rw [Set.image_subset_iff]
180+
exact (Filter.eventually_all_finite ht).mpr this
181+
intro y hy
182+
exact eventually_homothety_mem_of_mem_interior 𝕜 x (h hy)
183+
#align eventually_homothety_image_subset_of_finite_subset_interior eventually_homothety_image_subset_of_finite_subset_interior
184+
185+
end NormedSpace
186+
187+
variable [NormedSpace ℝ V] [NormedSpace ℝ W]
188+
189+
theorem dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
190+
dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2 := by
191+
-- Porting note: was `simpa using dist_midpoint_midpoint_le' p₁ p₂ p₃ p₄`
192+
have := dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄
193+
rw [Real.norm_eq_abs, abs_two] at this
194+
exact this
195+
#align dist_midpoint_midpoint_le dist_midpoint_midpoint_le
196+
197+
/-- A continuous map between two normed affine spaces is an affine map provided that
198+
it sends midpoints to midpoints. -/
199+
def AffineMap.ofMapMidpoint (f : P → Q) (h : ∀ x y, f (midpoint ℝ x y) = midpoint ℝ (f x) (f y))
200+
(hfc : Continuous f) : P →ᵃ[ℝ] Q :=
201+
let c := Classical.arbitrary P
202+
AffineMap.mk' f (↑((AddMonoidHom.ofMapMidpoint ℝ ℝ
203+
((AffineEquiv.vaddConst ℝ (f <| c)).symm ∘ f ∘ AffineEquiv.vaddConst ℝ c) (by simp)
204+
fun x y => by -- Porting note: was `by simp [h]`
205+
simp
206+
conv_lhs => rw [(midpoint_self ℝ (Classical.arbitrary P)).symm, midpoint_vadd_midpoint, h, h,
207+
midpoint_vsub_midpoint]).toRealLinearMap <| by
208+
apply_rules [Continuous.vadd, Continuous.vsub, continuous_const, hfc.comp, continuous_id]))
209+
c fun p => by simp
210+
#align affine_map.of_map_midpoint AffineMap.ofMapMidpoint

‎Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -220,11 +220,11 @@ def Simps.apply (e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂ :=
220220
#align affine_equiv.simps.apply AffineEquiv.Simps.apply
221221

222222
/-- See Note [custom simps projection] -/
223-
def Simps.symmApply (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁ :=
223+
def Simps.symm_apply (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁ :=
224224
e.symm
225-
#align affine_equiv.simps.symm_apply AffineEquiv.Simps.symmApply
225+
#align affine_equiv.simps.symm_apply AffineEquiv.Simps.symm_apply
226226

227-
initialize_simps_projections AffineEquiv (toEquiv_toFun → apply, toEquiv_invFun → symmApply,
227+
initialize_simps_projections AffineEquiv (toEquiv_toFun → apply, toEquiv_invFun → symm_apply,
228228
linear → linear, as_prefix linear, -toEquiv)
229229

230230
protected theorem bijective (e : P₁ ≃ᵃ[k] P₂) : Bijective e :=
@@ -451,7 +451,7 @@ variable (k)
451451

452452
/-- The map `v ↦ v +ᵥ b` as an affine equivalence between a module `V` and an affine space `P` with
453453
tangent space `V`. -/
454-
@[simps! linear apply]
454+
@[simps! linear apply symm_apply]
455455
def vaddConst (b : P₁) : V₁ ≃ᵃ[k] P₁ where
456456
toEquiv := Equiv.vaddConst b
457457
linear := LinearEquiv.refl _ _

0 commit comments

Comments
 (0)