 105  omega
 106
 107/-- maxOctantLevel n ≤ n (since log2(n+1)/3 ≤ log2(n+1) ≤ n). -/
 108lemma maxOctantLevel_le (n : Nat) : maxOctantLevel n ≤ n := by
 109  unfold maxOctantLevel
 110  have h1 : Nat.log2 n.succ / 3 ≤ Nat.log2 n.succ := Nat.div_le_self _ _
 111  have h2 : Nat.log2 n.succ ≤ n := log2_succ_le n
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.