E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
⊢ ∃ c', (∀ (n : Fin (Nat.succ N)), ‖c' n‖ ≤ 2) ∧ ∀ (i j : Fin (Nat.succ N)), i ≠ j → 1 - δ ≤ ‖c' i - c' j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
⊢ ∃ c', (∀ (n : Fin (Nat.succ N)), ‖c' n‖ ≤ 2) ∧ ∀ (i j : Fin (Nat.succ N)), i ≠ j → 1 - δ ≤ ‖c' i - c' j‖
let c' : Fin N.succ → E := fun i => if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
⊢ 1 - δ ≤ ‖c' i - c' j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
⊢ ∃ c', (∀ (n : Fin (Nat.succ N)), ‖c' n‖ ≤ 2) ∧ ∀ (i j : Fin (Nat.succ N)), i ≠ j → 1 - δ ≤ ‖c' i - c' j‖
refine' ⟨c', fun n => norm_c'_le n, fun i j inej => _⟩
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
this : ∀ (i j : Fin (Nat.succ N)), i ≠ j → ‖c a i‖ ≤ ‖c a j‖ → 1 - δ ≤ ‖c' i - c' j‖
hij : ¬‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
⊢ 1 - δ ≤ ‖c' i - c' j‖
wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : ‖c a j‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
rcases le_or_lt ‖a.c j‖ 2 with (Hj | Hj)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
⊢ ‖c' i‖ ≤ 2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
⊢ ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
intro i
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
⊢ ‖if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i‖ ≤ 2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
⊢ ‖c' i‖ ≤ 2
simp only
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ‖c a i‖ ≤ 2
⊢ ‖c a i‖ ≤ 2

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ¬‖c a i‖ ≤ 2
⊢ ‖(2 / ‖c a i‖) • c a i‖ ≤ 2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
⊢ ‖if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i‖ ≤ 2
split_ifs with h
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ¬‖c a i‖ ≤ 2
hi : ‖c a i‖ = 0
⊢ 0 ≤ 2
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ¬‖c a i‖ ≤ 2
⊢ ‖(2 / ‖c a i‖) • c a i‖ ≤ 2
by_cases hi : ‖a.c i‖ = 0 <;> field_simp [norm_smul, hi]
no goals
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ¬‖c a i‖ ≤ 2
hi : ‖c a i‖ = 0
⊢ 0 ≤ 2
norm_num
no goals
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
i : Fin (Nat.succ N)
h : ‖c a i‖ ≤ 2
⊢ ‖c a i‖ ≤ 2
exact h
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
this : ∀ (i j : Fin (Nat.succ N)), i ≠ j → ‖c a i‖ ≤ ‖c a j‖ → 1 - δ ≤ ‖c' i - c' j‖
hij : ¬‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' j - c' i‖
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
this : ∀ (i j : Fin (Nat.succ N)), i ≠ j → ‖c a i‖ ≤ ‖c a j‖ → 1 - δ ≤ ‖c' i - c' j‖
hij : ¬‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
rw [norm_sub_rev]
no goals
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
this : ∀ (i j : Fin (Nat.succ N)), i ≠ j → ‖c a i‖ ≤ ‖c a j‖ → 1 - δ ≤ ‖c' i - c' j‖
hij : ¬‖c a i‖ ≤ ‖c a j‖
⊢ 1 - δ ≤ ‖c' j - c' i‖
exact this j i inej.symm (le_of_not_le hij)
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : ‖c a j‖ ≤ 2
⊢ 1 - δ ≤ ‖c a i - c a j‖
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : ‖c a j‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖
simp_rw [Hj, hij.trans Hj, if_true]
no goals
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : ‖c a j‖ ≤ 2
⊢ 1 - δ ≤ ‖c a i - c a j‖
exact exists_normalized_aux1 a lastr hτ δ hδ1 hδ2 i j inej
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have H'j : ‖a.c j‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false_iff] using Hj
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : ‖c a i‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖

case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖
rcases le_or_lt ‖a.c i‖ 2 with (Hi | Hi)
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
⊢ ‖c a j‖ ≤ 2 ↔ False
simpa only [not_le, iff_false_iff] using Hj
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : ‖c a i‖ ≤ 2
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : ‖c a i‖ ≤ 2
⊢ 1 - δ ≤ ‖c' i - c' j‖
simp_rw [Hi, if_true, H'j, if_false]
no goals
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : ‖c a i‖ ≤ 2
⊢ 1 - δ ≤ ‖c a i - (2 / ‖c a j‖) • c a j‖
exact exists_normalized_aux2 a lastc lastr hτ δ hδ1 hδ2 i j inej Hi Hj
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
H'i : ‖c a i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have H'i : ‖a.c i‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false_iff] using Hi
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
H'i : ‖c a i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖(2 / ‖c a i‖) • c a i - (2 / ‖c a j‖) • c a j‖
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
H'i : ‖c a i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖c' i - c' j‖
simp_rw [H'i, if_false, H'j, if_false]
no goals
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
H'i : ‖c a i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖(2 / ‖c a i‖) • c a i - (2 / ‖c a j‖) • c a j‖
exact exists_normalized_aux3 a lastc lastr hτ δ hδ1 i j inej Hi hij
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : c a (last N) = 0
lastr : r a (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin (Nat.succ N) → E := fun i => if ‖c a i‖ ≤ 2 then c a i else (2 / ‖c a i‖) • c a i
norm_c'_le : ∀ (i : Fin (Nat.succ N)), ‖c' i‖ ≤ 2
i j : Fin (Nat.succ N)
inej : i ≠ j
hij : ‖c a i‖ ≤ ‖c a j‖
Hj : 2 < ‖c a j‖
H'j : ‖c a j‖ ≤ 2 ↔ False
Hi : 2 < ‖c a i‖
⊢ ‖c a i‖ ≤ 2 ↔ False
simpa only [not_le, iff_false_iff] using Hi