diff --git a/src/algebra/add_torsor.lean b/src/algebra/add_torsor.lean index 0aabd62f4251d..305ab5b51135e 100644 --- a/src/algebra/add_torsor.lean +++ b/src/algebra/add_torsor.lean @@ -114,6 +114,9 @@ equal. -/ @[simp] lemma vsub_eq_zero_iff_eq {p1 p2 : P} : p1 -ᵥ p2 = (0 : G) ↔ p1 = p2 := iff.intro eq_of_vsub_eq_zero (λ h, h ▸ vsub_self _) +lemma vsub_ne_zero {p q : P} : p -ᵥ q ≠ (0 : G) ↔ p ≠ q := +not_congr vsub_eq_zero_iff_eq + /-- Cancellation adding the results of two subtractions. -/ @[simp] lemma vsub_add_vsub_cancel (p1 p2 p3 : P) : p1 -ᵥ p2 + (p2 -ᵥ p3) = (p1 -ᵥ p3) := begin @@ -129,6 +132,9 @@ begin rw [vsub_add_vsub_cancel, vsub_self], end +lemma vadd_vsub_eq_sub_vsub (g : G) (p q : P) : g +ᵥ p -ᵥ q = g - (q -ᵥ p) := +by rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev] + /-- Subtracting the result of adding a group element produces the same result as subtracting the points and subtracting that group element. -/ lemma vsub_vadd_eq_vsub_sub (p1 p2 : P) (g : G) : p1 -ᵥ (g +ᵥ p2) = (p1 -ᵥ p2) - g := diff --git a/src/analysis/normed/group/basic.lean b/src/analysis/normed/group/basic.lean index 00a094416dda8..a34f62164d5dc 100644 --- a/src/analysis/normed/group/basic.lean +++ b/src/analysis/normed/group/basic.lean @@ -256,6 +256,9 @@ lemma norm_le_add_norm_add (u v : E) : calc ∥u∥ = ∥u + v - v∥ : by rw add_sub_cancel ... ≤ ∥u + v∥ + ∥v∥ : norm_sub_le _ _ +lemma ball_eq (y : E) (ε : ℝ) : metric.ball y ε = { x | ∥x - y∥ < ε} := +by { ext, simp [dist_eq_norm], } + lemma ball_zero_eq (ε : ℝ) : ball (0 : E) ε = {x | ∥x∥ < ε} := set.ext $ assume a, by simp @@ -425,6 +428,20 @@ lemma normed_group.cauchy_seq_iff [nonempty α] [semilattice_sup α] {u : α → cauchy_seq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ∥u m - u n∥ < ε := by simp [metric.cauchy_seq_iff, dist_eq_norm] +lemma normed_group.nhds_basis_norm_lt (x : E) : + (𝓝 x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), { y | ∥y - x∥ < ε }) := +begin + simp_rw ← ball_eq, + exact metric.nhds_basis_ball, +end + +lemma normed_group.nhds_zero_basis_norm_lt : + (𝓝 (0 : E)).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), { y | ∥y∥ < ε }) := +begin + convert normed_group.nhds_basis_norm_lt (0 : E), + simp, +end + lemma normed_group.uniformity_basis_dist : (𝓤 E).has_basis (λ (ε : ℝ), 0 < ε) (λ ε, {p : E × E | ∥p.fst - p.snd∥ < ε}) := begin diff --git a/src/analysis/normed_space/add_torsor.lean b/src/analysis/normed_space/add_torsor.lean index 3d57b8dd8422e..3d45e713ff013 100644 --- a/src/analysis/normed_space/add_torsor.lean +++ b/src/analysis/normed_space/add_torsor.lean @@ -24,11 +24,11 @@ variables {W Q : Type*} [normed_group W] [metric_space Q] [normed_add_torsor W Q section normed_space -variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V] +variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V] [normed_space 𝕜 W] open affine_map -lemma affine_subspace.is_closed_direction_iff [normed_space 𝕜 W] (s : affine_subspace 𝕜 Q) : +lemma affine_subspace.is_closed_direction_iff (s : affine_subspace 𝕜 Q) : is_closed (s.direction : set W) ↔ is_closed (s : set Q) := begin rcases s.eq_bot_or_nonempty with rfl|⟨x, hx⟩, { simp [is_closed_singleton] }, @@ -60,15 +60,6 @@ lemma lipschitz_with_line_map (p₁ p₂ : P) : lipschitz_with.of_dist_le_mul $ λ c₁ c₂, ((dist_line_map_line_map p₁ p₂ c₁ c₂).trans (mul_comm _ _)).le -omit V - -lemma antilipschitz_with_line_map [normed_space 𝕜 W] {p₁ p₂ : Q} (h : p₁ ≠ p₂) : - antilipschitz_with (nndist p₁ p₂)⁻¹ (line_map p₁ p₂ : 𝕜 → Q) := -antilipschitz_with.of_le_mul_dist $ λ c₁ c₂, by rw [dist_line_map_line_map, nnreal.coe_inv, - ← dist_nndist, mul_left_comm, inv_mul_cancel (dist_ne_zero.2 h), mul_one] - -include V - @[simp] lemma dist_line_map_left (p₁ p₂ : P) (c : 𝕜) : dist (line_map p₁ p₂ c) p₁ = ∥c∥ * dist p₁ p₂ := by simpa only [line_map_apply_zero, dist_zero_right] using dist_line_map_line_map p₁ p₂ c 0 @@ -93,6 +84,8 @@ by rw [homothety_eq_line_map, dist_line_map_right] dist p₂ (homothety p₁ c p₂) = ∥1 - c∥ * dist p₁ p₂ := by rw [dist_comm, dist_homothety_self] +section invertible_two + variables [invertible (2:𝕜)] @[simp] lemma dist_left_midpoint (p₁ p₂ : P) : @@ -120,6 +113,40 @@ begin exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _), end +end invertible_two + +omit V +include W + +lemma antilipschitz_with_line_map {p₁ p₂ : Q} (h : p₁ ≠ p₂) : + antilipschitz_with (nndist p₁ p₂)⁻¹ (line_map p₁ p₂ : 𝕜 → Q) := +antilipschitz_with.of_le_mul_dist $ λ c₁ c₂, by rw [dist_line_map_line_map, nnreal.coe_inv, + ← dist_nndist, mul_left_comm, inv_mul_cancel (dist_ne_zero.2 h), mul_one] + +lemma eventually_homothety_mem_of_mem_interior (x : Q) {s : set Q} {y : Q} (hy : y ∈ interior s) : + ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s := +begin + rw (normed_group.nhds_basis_norm_lt (1 : 𝕜)).eventually_iff, + cases eq_or_ne y x with h h, { use 1, simp [h.symm, interior_subset hy], }, + have hxy : 0 < ∥y -ᵥ x∥, { rwa [norm_pos_iff, vsub_ne_zero], }, + obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy, + obtain ⟨ε, hε, hyε⟩ := metric.is_open_iff.mp hu₂ y hu₃, + refine ⟨ε / ∥y -ᵥ x∥, div_pos hε hxy, λ δ (hδ : ∥δ - 1∥ < ε / ∥y -ᵥ x∥), hu₁ (hyε _)⟩, + rw [lt_div_iff hxy, ← norm_smul, sub_smul, one_smul] at hδ, + rwa [homothety_apply, metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub], +end + +lemma eventually_homothety_image_subset_of_finite_subset_interior + (x : Q) {s : set Q} {t : set Q} (ht : t.finite) (h : t ⊆ interior s) : + ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ '' t ⊆ s := +begin + suffices : ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s, + { simp_rw set.image_subset_iff, + exact (filter.eventually_all_finite ht).mpr this, }, + intros y hy, + exact eventually_homothety_mem_of_mem_interior x (h hy), +end + end normed_space variables [normed_space ℝ V] [normed_space ℝ W]