structure Noperthedron.Solution.Row.ValidSplitParam (tab : Table) (row : Row) (param : Param) : Prop

• bound0 : row.ID < row.IDfirstChild
• bound1 : row.IDfirstChild < Array.size tab
• bound2 : row.IDfirstChild + 1 < Array.size tab
• first_child_good : tab[row.IDfirstChild].interval = Interval.lower_half param row.interval
• second_child_good : tab[row.IDfirstChild + 1].interval = Interval.upper_half param row.interval

theorem Noperthedron.Solution.Row.validSplitParam_iff (tab : Table) (row : Row) (param : Param) : ValidSplitParam tab row param ↔ row.ID < row.IDfirstChild ∧ ∃ (bound1 : row.IDfirstChild < Array.size tab) (bound2 : row.IDfirstChild + 1 < Array.size tab), tab[row.IDfirstChild].interval = Interval.lower_half param row.interval ∧ tab[row.IDfirstChild + 1].interval = Interval.upper_half param row.interval

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValidSplitParam (tab : Table) (row : Row) (param : Param) : Decidable (Row.ValidSplitParam tab row param)

Equations

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

def Noperthedron.Solution.Row.ValidBinarySplit (tab : Table) (row : Row) : Prop

Equations

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

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidBinarySplit (tab : Table) (row : Row) : Decidable (ValidBinarySplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidBinarySplit tab row = Noperthedron.Solution.Row.instDecidableValidBinarySplit._aux_1 tab row

def Noperthedron.Solution.Table.HasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) : Prop

Equations

• tab.HasIntervals start intervals = ∀ (i : Fin intervals.length), ∃ (h : start + ↑i < Array.size tab), tab[start + ↑i].interval = intervals[i]

@[implicit_reducible]

instance Noperthedron.Solution.Table.instDecidableHasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) : Decidable (tab.HasIntervals start intervals)

Equations

• tab.instDecidableHasIntervals start intervals = Noperthedron.Solution.Table.instDecidableHasIntervals._aux_1 tab start intervals

def Noperthedron.Solution.Row.ValidFullSplit (tab : Table) (row : Row) : Prop

Equations

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

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidFullSplit (tab : Table) (row : Row) : Decidable (ValidFullSplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidFullSplit tab row = Noperthedron.Solution.Row.instDecidableValidFullSplit._aux_1 tab row

def Noperthedron.Solution.Row.ValidSplit (tab : Table) (row : Row) : Prop

Equations

• Noperthedron.Solution.Row.ValidSplit tab row = (row.nodeType = 3 ∧ (Noperthedron.Solution.Row.ValidBinarySplit tab row ∨ Noperthedron.Solution.Row.ValidFullSplit tab row))

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidSplit (tab : Table) (row : Row) : Decidable (ValidSplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidSplit tab row = Noperthedron.Solution.Row.instDecidableValidSplit._aux_1 tab row

inductive Noperthedron.Solution.Row.Valid (tab : Table) (row : Row) : Prop

• asSplit {tab : Table} {row : Row} : ValidSplit tab row → Valid tab row
• asGlobal {tab : Table} {row : Row} : row.ValidGlobal → Valid tab row
• asLocal {tab : Table} {row : Row} : row.ValidLocal → Valid tab row

theorem Noperthedron.Solution.Row.valid_iff (tab : Table) (row : Row) : Valid tab row ↔ ValidSplit tab row ∨ row.ValidGlobal ∨ row.ValidLocal

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValid (tab : Table) (row : Row) : Decidable (Row.Valid tab row)

Equations

• Noperthedron.Solution.instDecidableValid tab row = decidable_of_iff (Noperthedron.Solution.Row.ValidSplit tab row ∨ row.ValidGlobal ∨ row.ValidLocal) ⋯

def Noperthedron.Solution.Row.ValidIx (tab : Table) (i : ℕ) (row : Row) : Prop

Equations

• Noperthedron.Solution.Row.ValidIx tab i row = (row.ID = i ∧ Noperthedron.Solution.Row.Valid tab row ∧ row.ID < Array.size tab)

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidIx (tab : Table) (i : ℕ) (row : Row) : Decidable (ValidIx tab i row)

Equations

• Noperthedron.Solution.Row.instDecidableValidIx tab i row = Noperthedron.Solution.Row.instDecidableValidIx._aux_1 tab i row

def Noperthedron.Solution.Table.Valid (tab : Table) : Prop

Equations

• tab.Valid = ∀ (i : Fin (Array.size tab)), Noperthedron.Solution.Row.ValidIx tab (↑i) tab[i]

@[implicit_reducible]

instance Noperthedron.Solution.Table.instDecidableValid (tab : Table) : Decidable tab.Valid

Equations

• tab.instDecidableValid = Noperthedron.Solution.Table.instDecidableValid._aux_1 tab

theorem Noperthedron.Solution.Table.Valid.valid_at {tab : Table} (htab : tab.Valid) {i : ℕ} (hi : i < Array.size tab) : Row.ValidIx tab i tab[i]

def Noperthedron.Solution.Table.valid_decidable (tab : Table) : Decidable tab.Valid

Equations

• tab.valid_decidable = inferInstance

def Noperthedron.Solution.Interval.minPose (iv : Interval) : Pose ℝ

The minimum endpoint of an Interval, viewed as a Pose ℝ via Rat.cast.

Equations

• iv.minPose = { θ₁ := ↑(PoseInterval.min iv).θ₁, θ₂ := ↑(PoseInterval.min iv).θ₂, φ₁ := ↑(PoseInterval.min iv).φ₁, φ₂ := ↑(PoseInterval.min iv).φ₂, α := ↑(PoseInterval.min iv).α }

def Noperthedron.Solution.Interval.maxPose (iv : Interval) : Pose ℝ

The maximum endpoint of an Interval, viewed as a Pose ℝ via Rat.cast.

Equations

• iv.maxPose = { θ₁ := ↑(PoseInterval.max iv).θ₁, θ₂ := ↑(PoseInterval.max iv).θ₂, φ₁ := ↑(PoseInterval.max iv).φ₁, φ₂ := ↑(PoseInterval.max iv).φ₂, α := ↑(PoseInterval.max iv).α }

def Noperthedron.Solution.Interval.toReal (iv : Interval) : PoseInterval ℝ

Equations

• iv.toReal = PoseInterval.mk iv.minPose iv.maxPose ⋯

def Noperthedron.Solution.Row.toRealInterval (row : Row) : PoseInterval ℝ

Equations

• row.toRealInterval = row.interval.toReal

theorem Noperthedron.Solution.Interval.toReal_center_getParam (iv : Interval) (p : Param) : iv.toReal.center.getParam p = ↑(iv.center p)

Each component of iv.toReal.center (real) is the Rat.cast of the corresponding iv.center (rational).

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_θ₁ (iv : Interval) : iv.toReal.center.θ₁ = ↑(iv.center Param.θ₁)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_θ₂ (iv : Interval) : iv.toReal.center.θ₂ = ↑(iv.center Param.θ₂)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_φ₁ (iv : Interval) : iv.toReal.center.φ₁ = ↑(iv.center Param.φ₁)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_φ₂ (iv : Interval) : iv.toReal.center.φ₂ = ↑(iv.center Param.φ₂)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_α (iv : Interval) : iv.toReal.center.α = ↑(iv.center Param.α)

@[implicit_reducible]

noncomputable instance Noperthedron.Solution.instCoeIntervalSetPoseReal : Coe Interval (Set (Pose ℝ))

The set of poses lying in the rational interval, defined as Set.Icc of the min/max endpoints; agrees definitionally with iv.toReal.

Equations

• Noperthedron.Solution.instCoeIntervalSetPoseReal = { coe := fun (iv : Noperthedron.Solution.Interval) => Set.Icc iv.minPose iv.maxPose }

theorem Noperthedron.Solution.cube_fold_nonempty_aux {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) : 0 < (cubeFold fs b as).length

theorem Noperthedron.Solution.cube_fold_nonempty {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) : 1 ≤ (cubeFold fs b as).length

theorem Noperthedron.Solution.cube_fold_halves (h : Param) (tl : List Param) (iv : Interval) (lower upper : Param → Interval → Interval) : cubeFold [lower, upper] iv (h :: tl) = cubeFold [lower, upper] (lower h iv) tl ++ cubeFold [lower, upper] (upper h iv) tl

theorem Noperthedron.Solution.has_intervals_start_in_table (tab : Table) (n : ℕ) (ivs : List Interval) (hivs : 1 ≤ ivs.length) (hi : tab.HasIntervals n ivs) : n < Array.size tab

theorem Noperthedron.Solution.has_intervals_concat (tab : Table) (start : ℕ) (ivs1 ivs2 : List Interval) : tab.HasIntervals start (ivs1 ++ ivs2) ↔ tab.HasIntervals start ivs1 ∧ tab.HasIntervals (start + ivs1.length) ivs2