FormalDepartures.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Formal departures and exact quotient increments of constant runs.

def OAI.TwoPointCorrelations.formalDeparture line 15
theorem OAI.TwoPointCorrelations.formalDeparture_const_run line 18

theorem OAI.TwoPointCorrelations.quotient_departure_const_run line 31

Source documentation

Every regular run moves parallel to its independent quotient direction.

theorem quotient_departure_const_run (D : Submodule K (α → K))
    (label : ℕ → α) (coefficient : ℕ → K)
    (a b : ℕ) (hab : a ≤ b) (z : α) (hz : ∀ i ∈ Ico a b, label i = z) :
    D.mkQ (formalDeparture label coefficient b) =
      D.mkQ (formalDeparture label coefficient a) +
        (∑ i ∈ Ico a b, coefficient i) • D.mkQ (Pi.basisFun K α z) := by
…

Mentions: OAI.TwoPointCorrelations.formalDeparture

theorem OAI.TwoPointCorrelations.affine_line_successor line 39
theorem OAI.TwoPointCorrelations.nonzero_direction_increment line 47
theorem OAI.TwoPointCorrelations.run_coefficient_ne_zero line 58
Source documentation
Scalar evaluation turns the formal displacement into the numerical one in a column. A nonzero numerical run forces a nonzero scalar sum.
```
theorem run_coefficient_ne_zero (coefficient : ℕ → K) (a b : ℕ) (prime : K)
    (hnonzero : (∑ i ∈ Ico a b, coefficient i * prime) ≠ 0) :
    (∑ i ∈ Ico a b, coefficient i) ≠ 0 := by
…
```

theorem OAI.TwoPointCorrelations.quotient_run_endpoints_ne line 67

Source documentation

A regular run has distinct quotient endpoints as required by the point--line--point non-reversal check.

theorem quotient_run_endpoints_ne (D : Submodule K (α → K))
    (label : ℕ → α) (coefficient : ℕ → K)
    (a b : ℕ) (hab : a ≤ b) (z : α) (hz : ∀ i ∈ Ico a b, label i = z)
    (hdir : D.mkQ (Pi.basisFun K α z) ≠ 0)
    (hc : (∑ i ∈ Ico a b, coefficient i) ≠ 0) :
    D.mkQ (formalDeparture label coefficient a) ≠ D.mkQ (formalDeparture label coefficient b) :=
…

Mentions: OAI.TwoPointCorrelations.formalDeparture