flatMap_length_bound'

formal source

 112  omega
 113
 114/-- Auxiliary: flatMap length bound. -/
 115private lemma flatMap_length_bound' (f : Nat → List (XORSystem n)) (m bound : Nat)
 116    (hbound : ∀ k < m, (f k).length ≤ bound) :
 117    ((List.range m).flatMap f).length ≤ m * bound := by
 118  rw [List.length_flatMap]
 119  have h : ∀ k ∈ List.range m, (f k).length ≤ bound := by
 120    intro k hk
 121    exact hbound k (List.mem_range.mp hk)
 122  have hsum : (List.map (fun k => (f k).length) (List.range m)).sum ≤
 123              (List.map (fun _ => bound) (List.range m)).sum := by
 124    apply List.sum_le_sum
 125    intro k hk
 126    exact h k hk
 127  calc ((List.map (fun k => (f k).length) (List.range m)).sum : Nat)
 128      ≤ (List.map (fun _ => bound) (List.range m)).sum := hsum
 129    _ = m * bound := by rw [List.map_const', List.sum_replicate, List.length_range]; ring
 130
 131/-- Morton octant family has polynomial size O(n²). -/
 132lemma mortonOctantFamily_size_bound (n : Nat) :
 133    (mortonOctantFamily n).length ≤ 2 * n.succ ^ 2 := by
 134  unfold mortonOctantFamily
 135  have hbound : ∀ level < maxOctantLevel n + 1, (octantsAtLevel n level).length ≤ 2 * (n + 1) :=
 136    fun level _ => octantsAtLevel_length_bound n level
 137  have h1 := flatMap_length_bound' (octantsAtLevel n) (maxOctantLevel n + 1) (2 * (n + 1)) hbound
 138  have h2 : maxOctantLevel n + 1 ≤ n + 1 := by
 139    have := maxOctantLevel_le n
 140    omega
 141  calc (mortonOctantFamily n).length
 142      = ((List.range (maxOctantLevel n + 1)).flatMap (octantsAtLevel n)).length := rfl
 143    _ ≤ (maxOctantLevel n + 1) * (2 * (n + 1)) := h1
 144    _ ≤ (n + 1) * (2 * (n + 1)) := Nat.mul_le_mul_right _ h2
 145    _ = 2 * (n + 1) ^ 2 := by ring