Lean4
/-- If there are no configurations of satellites with `N+1` points, one never uses more than `N`
distinct families in the Besicovitch inductive construction. -/
theorem color_lt {i : Ordinal.{u}} (hi : i < p.lastStep) {N : ℕ} (hN : IsEmpty (SatelliteConfig α N p.τ)) :
p.color i < N := by
/- By contradiction, consider the first ordinal `i` for which one would have `p.color i = N`.
Choose for each `k < N` a ball with color `k` that intersects the ball at color `i`
(there is such a ball, otherwise one would have used the color `k` and not `N`).
Then this family of `N+1` balls forms a satellite configuration, which is forbidden by
the assumption `hN`. -/
induction i using Ordinal.induction with
| _ i IH
let A : Set ℕ :=
⋃ (j : { j // j < i }) (_ :
(closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
{p.color j}
have color_i : p.color i = sInf (univ \ A) := by rw [color]
rw [color_i]
have N_mem : N ∈ univ \ A :=
by
simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and, mem_univ, mem_diff,
Subtype.exists]
intro j ji _
exact (IH j ji (ji.trans hi)).ne'
suffices sInf (univ \ A) ≠ N
by
rcases (csInf_le (OrderBot.bddBelow (univ \ A)) N_mem).lt_or_eq with (H | H)
· exact H
· exact (this H).elim
intro Inf_eq_N
have :
∀ k,
k < N →
∃ j,
j < i ∧
(closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
k = p.color j :=
by
intro k hk
rw [← Inf_eq_N] at hk
have : k ∈ A := by simpa only [true_and, mem_univ, Classical.not_not, mem_diff] using Nat.notMem_of_lt_sInf hk
simp only [] at this
simpa only [A, exists_prop, mem_iUnion, mem_singleton_iff, mem_closedBall, Subtype.exists, Subtype.coe_mk]
choose! g hg using this
let G : ℕ → Ordinal := fun n => if n = N then i else g n
have color_G : ∀ n, n ≤ N → p.color (G n) = n := by
intro n hn
rcases hn.eq_or_lt with (rfl | H)
· simp only [G]; simp only [color_i, Inf_eq_N, if_true]
· simp only [G]; simp only [H.ne, (hg n H).right.right.symm, if_false]
have G_lt_last : ∀ n, n ≤ N → G n < p.lastStep := by
intro n hn
rcases hn.eq_or_lt with (rfl | H)
· simp only [G]; simp only [hi, if_true]
· simp only [G]; simp only [H.ne, (hg n H).left.trans hi, if_false]
have fGn : ∀ n, n ≤ N → p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n)) :=
by
intro n hn
have : p.index (G n) = Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
rw [index]; rfl
rw [this]
have : ∃ t, p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
simpa only [not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq, not_forall] using
notMem_of_lt_csInf (G_lt_last n hn) (OrderBot.bddBelow _)
exact Classical.epsilon_spec this
have Gab :
∀ a b : Fin (Nat.succ N),
G a < G b →
p.r (p.index (G a)) ≤ dist (p.c (p.index (G a))) (p.c (p.index (G b))) ∧
p.r (p.index (G b)) ≤ p.τ * p.r (p.index (G a)) :=
by
intro a b G_lt
have ha : (a : ℕ) ≤ N := Nat.lt_succ_iff.1 a.2
have hb : (b : ℕ) ≤ N := Nat.lt_succ_iff.1 b.2
constructor
· have := (fGn b hb).1
simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and, Subtype.exists] at this
simpa only [dist_comm, mem_ball, not_lt] using this (G a) G_lt
· apply le_trans _ (fGn a ha).2
have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by intro H;
exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)
let b' : { t // p.c t ∉ p.iUnionUpTo (G a) } := ⟨p.index (G b), B⟩
apply @le_ciSup _ _ _ (fun t : { t // p.c t ∉ p.iUnionUpTo (G a) } => p.r t) _ b'
refine ⟨p.r_bound, fun t ht => ?_⟩
simp only [exists_prop, mem_range, Subtype.exists] at ht
rcases ht with ⟨u, hu⟩
rw [← hu.2]
exact
p.r_le
_
-- therefore, one may use them to construct a satellite configuration with `N+1` points
let sc : SatelliteConfig α N p.τ :=
{ c := fun k => p.c (p.index (G k))
r := fun k => p.r (p.index (G k))
rpos := fun k => p.rpos (p.index (G k))
h := by
intro a b a_ne_b
wlog G_le : G a ≤ G b generalizing a b
· exact (this a_ne_b.symm (le_of_not_ge G_le)).symm
have G_lt : G a < G b := by
rcases G_le.lt_or_eq with (H | H); · exact H
have A : (a : ℕ) ≠ b := Fin.val_injective.ne a_ne_b
rw [← color_G a (Nat.lt_succ_iff.1 a.2), ← color_G b (Nat.lt_succ_iff.1 b.2), H] at A
exact (A rfl).elim
exact Or.inl (Gab a b G_lt)
hlast := by
intro a ha
have I : (a : ℕ) < N := ha
have : G a < G (Fin.last N) := by simp [G, I.ne, (hg a I).1]
exact Gab _ _ this
inter := by
intro a ha
have I : (a : ℕ) < N := ha
have J : G (Fin.last N) = i := by dsimp; simp only [G, if_true]
have K : G a = g a := by simp [G, I.ne]
convert dist_le_add_of_nonempty_closedBall_inter_closedBall (hg _ I).2.1 }
-- this is a contradiction
exact hN.false sc
