IndisputableMonolith.Causality.BallP

   1import Mathlib
   2import IndisputableMonolith.Causality.Basic
   3
   4namespace IndisputableMonolith
   5namespace Causality
   6
   7variable {α : Type}
   8
   9/-- `ballP K x n y` means y is within ≤ n steps of x via `K.step`. -/
  10def ballP (K : Kinematics α) (x : α) : Nat → α → Prop
  11| 0, y => y = x
  12| Nat.succ n, y => ballP K x n y ∨ ∃ z, ballP K x n z ∧ K.step z y
  13
  14lemma ballP_mono {K : Kinematics α} {x : α} {n m : Nat}
  15  (hnm : n ≤ m) : {y | ballP K x n y} ⊆ {y | ballP K x m y} := by
  16  induction hnm with
  17  | refl => intro y hy; simpa using hy
  18  | @step m hm ih =>
  19      intro y hy
  20      exact Or.inl (ih hy)
  21
  22lemma reach_mem_ballP {K : Kinematics α} {x y : α} :
  23  ∀ {n}, ReachN K n x y → ballP K x n y := by
  24  intro n h; induction h with
  25  | zero => simp [ballP]
  26  | @succ n x y z hxy hyz ih =>
  27      exact Or.inr ⟨y, ih, hyz⟩
  28
  29lemma inBall_subset_ballP {K : Kinematics α} {x y : α} {n : Nat} :
  30  inBall K x n y → ballP K x n y := by
  31  intro ⟨k, hk, hreach⟩
  32  have : ballP K x k y := reach_mem_ballP (K:=K) (x:=x) (y:=y) hreach
  33  exact (ballP_mono (K:=K) (x:=x) hk) this
  34
  35lemma ballP_subset_inBall {K : Kinematics α} {x y : α} :
  36  ∀ {n}, ballP K x n y → inBall K x n y := by
  37  intro n
  38  induction n generalizing y with
  39  | zero =>
  40      intro hy; rcases hy with rfl; exact ⟨0, le_rfl, ReachN.zero⟩
  41  | succ n ih =>
  42      intro hy
  43      cases hy with
  44      | inl hy' =>
  45          rcases ih hy' with ⟨k, hk, hkreach⟩
  46          exact ⟨k, Nat.le_trans hk (Nat.le_succ _), hkreach⟩
  47      | inr h' =>
  48          rcases h' with ⟨z, hz, hstep⟩
  49          rcases ih hz with ⟨k, hk, hkreach⟩
  50          exact ⟨k + 1, Nat.succ_le_succ hk, ReachN.succ hkreach hstep⟩
  51
  52end Causality
  53end IndisputableMonolith
  54