Segments.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ForestSpace.ForestOrder line 14
Source documentation
Every ancestral cone is a chain, the order-theoretic forest condition.
```
def ForestOrder (V : Type) [PartialOrder V] : Prop :=
…
```
def OAI.ForestSpace.IsSegment line 18
Source documentation
A finite, order-convex chain. The empty chain is a harmless zero test.
Also declared: ComparatorChallenges/ForestSpace.lean:73 (same declaration text).
```
def IsSegment {V : Type} [PartialOrder V] (S : Finset V) : Prop :=
…
```
def OAI.ForestSpace.segSum line 23
Source documentation
The sum of coordinates over a segment.
Also declared: ComparatorChallenges/ForestSpace.lean:78 (same declaration text).
```
def segSum {V : Type} (u : V → ℝ) (S : Finset V) : ℝ := ∑ v ∈ S, u v
```
def OAI.ForestSpace.TestBound line 26
Source documentation
Squared bound on every disjoint family of segment tests.
Also declared: ComparatorChallenges/ForestSpace.lean:81 (same declaration text).
```
def TestBound {V : Type} [PartialOrder V] (u : V → ℝ) (C : ℝ) : Prop :=
…
```
theorem OAI.ForestSpace.isSegment_empty line 34
theorem OAI.ForestSpace.isSegment_singleton line 37
theorem OAI.ForestSpace.segSum_empty line 51
theorem OAI.ForestSpace.segSum_zero line 53
theorem OAI.ForestSpace.segSum_add line 56
theorem OAI.ForestSpace.segSum_sub line 60
theorem OAI.ForestSpace.segSum_smul line 64
theorem OAI.ForestSpace.TestBound.mono line 68
theorem OAI.ForestSpace.TestBound.nonneg line 71
theorem OAI.ForestSpace.TestBound.single line 74
theorem OAI.ForestSpace.TestBound.zero line 79
theorem OAI.ForestSpace.TestBound.smul line 83
theorem OAI.ForestSpace.TestBound.add line 89

theorem OAI.ForestSpace.IsSegment.head line 116

Source documentation

Cutting a segment by an ancestral set produces another segment.

 theorem IsSegment.head {S : Finset V} (hS : IsSegment S) (H : Set V)
    (hH : IsLowerSet H) [DecidablePred (· ∈ H)] :
    IsSegment (S.filter (· ∈ H)) := by
…

Mentions: OAI.ForestSpace.IsSegment

theorem OAI.ForestSpace.IsSegment.tail line 126
theorem OAI.ForestSpace.TestBound.restrict line 137
theorem OAI.ForestSpace.TestBound.restrict_compl line 146
theorem OAI.ForestSpace.IsSegment.endpoints line 160
def OAI.ForestSpace.Gate line 174
Source documentation
A first vertex outside an ancestral set (including unattached roots).
```
def Gate (H : Set V) (g : V) : Prop := g ∉ H ∧ ∀ v, v < g → v ∈ H
```
theorem OAI.ForestSpace.Gate.eq_of_le line 176
theorem OAI.ForestSpace.IsSegment.gate_unique line 181
theorem OAI.ForestSpace.IsSegment.exists_gate line 187
def OAI.ForestSpace.SupportedOn line 210
Source documentation
A coordinate vector supported on a specified set.
```
def SupportedOn (u : V → ℝ) (H : Set V) : Prop := ∀ v, v ∉ H → u v = 0
…
```
theorem OAI.ForestSpace.SupportedOn.segSum_filter line 213
theorem OAI.ForestSpace.SupportedOn.segSum_eq_zero line 224
theorem OAI.ForestSpace.cross_zero_of_no_gate line 228