FiniteGeometry.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ForestSpace.before line 17
Source documentation
The ancestral interval [a,g), ending immediately before g along its path.
```
noncomputable def before (a g : V) : Finset V := by
…
```
theorem OAI.ForestSpace.mem_before line 21
theorem OAI.ForestSpace.isSegment_before line 25
theorem OAI.ForestSpace.before_mono line 33
theorem OAI.ForestSpace.before_subset_head line 37
theorem OAI.ForestSpace.IsSegment.head_eq_before line 42
theorem OAI.ForestSpace.IsSegment.sdiff_before line 65
Source documentation
Removing a terminal suffix from any segment leaves a segment.
```
 theorem IsSegment.sdiff_before {S : Finset V} (hS : IsSegment S) {a b g : V}
    (hSa : S = before a g) : IsSegment (S \ before b g) := by
…
```
Mentions: OAI.ForestSpace.IsSegment, OAI.ForestSpace.before
def OAI.ForestSpace.along line 81
Source documentation
The closed ancestral interval [g,w].
```
noncomputable def along (g w : V) : Finset V :=
…
```
theorem OAI.ForestSpace.mem_along line 84
theorem OAI.ForestSpace.isSegment_along line 87
theorem OAI.ForestSpace.IsSegment.tail_eq_along line 94
def OAI.ForestSpace.mass line 112
Source documentation
Maximal initial-segment mass of a test inside the cone at g.
```
noncomputable def mass (k : V → ℝ) (g : V) : ℝ :=
…
```
theorem OAI.ForestSpace.abs_segSum_along_le line 115
theorem OAI.ForestSpace.mass_nonneg line 119
theorem OAI.ForestSpace.mass_attained line 122
theorem OAI.ForestSpace.gate_mass_bound line 128
def OAI.ForestSpace.gateWeight line 144
Source documentation
Square mass at gates, and zero elsewhere.
```
noncomputable def gateWeight (H : Set V) (k : V → ℝ) (g : V) : ℝ :=
…
```
theorem OAI.ForestSpace.gateWeight_nonneg line 147
theorem OAI.ForestSpace.gateWeight_sum_le line 151
theorem OAI.ForestSpace.disjoint_sum_le line 161
theorem OAI.ForestSpace.gateWeight_family_le line 167

theorem OAI.ForestSpace.sum_gate_supported line 175

Source documentation

A segment contains at most one coordinate of a gate-supported vector.

 theorem sum_gate_supported [Fintype V] [PartialOrder V] {H : Set V} {c : V → ℝ}
    (hc : ∀ v, ¬ Gate H v → c v = 0) {S : Finset V} (hS : IsSegment S)
    {g : V} (hg : Gate H g) (hgs : g ∈ S) : segSum c S = c g := by
…

Mentions: OAI.ForestSpace.Gate, OAI.ForestSpace.IsSegment, OAI.ForestSpace.segSum

def OAI.ForestSpace.correction line 185
theorem OAI.ForestSpace.correction_supported line 188
theorem OAI.ForestSpace.correction_sum line 194
theorem OAI.ForestSpace.correction_segment_sq line 200
theorem OAI.ForestSpace.correction_testBound line 224
theorem OAI.ForestSpace.tail_sum_le_mass line 230
def OAI.ForestSpace.largeStarts line 240
Source documentation
Candidate starts of suffixes whose head sum reaches the gate threshold.
```
noncomputable def largeStarts (f k : V → ℝ) (s : ℝ) (g : V) : Finset V :=
…
```
theorem OAI.ForestSpace.mem_largeStarts line 243
def OAI.ForestSpace.selectedStart line 247
theorem OAI.ForestSpace.selectedStart_spec line 251
def OAI.ForestSpace.selectedHead line 256
theorem OAI.ForestSpace.selectedHead_segment line 259
theorem OAI.ForestSpace.selectedHead_subset line 266
theorem OAI.ForestSpace.selectedHead_large line 275
theorem OAI.ForestSpace.sdiff_selectedHead_segment line 282
def OAI.ForestSpace.oppositeSign line 294
Source documentation
Opposite sign for the selected head sum; at zero either sign is harmless.
```
def oppositeSign (r : ℝ) : ℝ := if r < 0 then 1 else -1
```
theorem OAI.ForestSpace.oppositeSign_sq line 296
theorem OAI.ForestSpace.abs_oppositeSign line 300
theorem OAI.ForestSpace.oppositeSign_cross line 304
theorem OAI.ForestSpace.oppositeSign_tail_abs line 312
theorem OAI.ForestSpace.small_cross_bound line 319
theorem OAI.ForestSpace.cross_sign line 328

theorem OAI.ForestSpace.large_cross_bound line 341

Source documentation

A large positive cross term is paid for by splitting off the selected suffix.

 theorem large_cross_bound {a b r s m : ℝ} (hs : 0 ≤ s) (hm : 0 ≤ m)
    (hab : 0 < a * b) (hrb : r * b ≤ 0) (hr : 2 * s * m ≤ |r|)
    (hb : |b| ≤ 2 * m) :
    2 * s * a * b ≤ (a - r) ^ 2 + r ^ 2 - a ^ 2 := by
…