Binary splitting of dyadic real intervals

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

def Inclusion.IntervalDyadicReal.midpoint (a b : Dyadic) : Dyadic

The midpoint of a and b.

Equations

• Inclusion.IntervalDyadicReal.midpoint a b = match a + b with | Dyadic.zero => Dyadic.zero | Dyadic.ofOdd n k hn => Dyadic.ofOdd n (k + 1) hn

@[specialize #[]]

def Inclusion.IntervalDyadicReal.binarySplitMap {Iβ : Type u_1} {β : Type u_2} [ToSet Iβ β] [Coarsen Iβ β] : ℕ → Interval Dyadic → (Interval Dyadic → 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.IntervalDyadicReal.binarySplitMap 0 x✝¹ x✝ = x✝ x✝¹
• Inclusion.IntervalDyadicReal.binarySplitMap n.succ x✝¹ x✝ = x✝ x✝¹

theorem Inclusion.IntervalDyadicReal.mem_binarySplitMap {Iβ : Type u_1} {β : Type u_2} [ToSet Iβ β] [Coarsen Iβ β] (n : ℕ) {I : Interval Dyadic} {F : Interval Dyadic → Iβ} {y : β} {r : ℝ} (hr : r ∈ I) (hy : ∀ (J : Interval Dyadic), r ∈ J → y ∈ F J) : y ∈ binarySplitMap n I F

def Inclusion.IntervalDyadicReal.binarySplit (n : ℕ) : Cover (Interval Dyadic) ℝ

Cover a dyadic interval by repeatedly bisecting it to depth n.

Equations

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

def Inclusion.IntervalDyadicReal.binarySplitParam : InclusionParamDecl

The depth to which bounded dyadic intervals are repeatedly bisected. A depth of n produces 2 ^ n pieces.

Equations

• Inclusion.IntervalDyadicReal.binarySplitParam = { name := `binSplit, type := q(ℕ) }

def Inclusion.IntervalDyadicReal.mkBinarySplitCover : InclusionM (Option Lean.Expr)

Construct the binary-splitting cover with 2 ^ n pieces.

Equations

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