Binary splitting of integer intervals

This file defines the binarySplit cover for the interval_int inclusion family.

@[specialize #[]]

def Inclusion.IntervalInt.binarySplitMap {Iβ : Type u_1} {β : Type u_2} [ToSet Iβ β] [Coarsen Iβ β] : ℕ → Interval ℤ → (Interval ℤ → Iβ) → Iβ

Map F over the intervals produced by bisecting I to depth n, coarsening the results.

Equations

• One or more equations did not get rendered due to their size.
• Inclusion.IntervalInt.binarySplitMap 0 x✝¹ x✝ = x✝ x✝¹
• Inclusion.IntervalInt.binarySplitMap n.succ x✝¹ x✝ = x✝ x✝¹

theorem Inclusion.IntervalInt.mem_binarySplitMap {Iβ : Type u_1} {β : Type u_2} [ToSet Iβ β] [Coarsen Iβ β] (n : ℕ) {I : Interval ℤ} {F : Interval ℤ → Iβ} {y : β} {x : ℤ} (hx : x ∈ I) (hy : ∀ (J : Interval ℤ), x ∈ J → y ∈ F J) : y ∈ binarySplitMap n I F

def Inclusion.IntervalInt.binarySplit (n : ℕ) : Cover (Interval ℤ) ℤ

Cover an integer interval by repeatedly bisecting it to depth n.

Equations

• One or more equations did not get rendered due to their size.