WeightedColumnBasis.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

+# Maximizing bases and normalized box coefficients

This is the basis-exchange step in the manuscript's box calculus. A nonzero coefficient permits column replacement. Maximality of the basis weight then makes the exponential rescaling factor at most one.

def OAI.PolycyclicRecognition.columnBasisMatrix line 24
Source documentation
The columns chosen from a finite list of vectors.
```
def columnBasisMatrix (v : I → Fin n → ℝ) (b : Fin n → I) : Matrix (Fin n) (Fin n) ℝ :=
…
```
def OAI.PolycyclicRecognition.columnBasisWeight line 27
def OAI.PolycyclicRecognition.IsMaximizingColumnBasis line 30
Source documentation
A genuine invertible column basis maximizing the prescribed total weight.
```
def IsMaximizingColumnBasis (v : I → Fin n → ℝ) (w : I → ℝ) (b : Fin n → I) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.exists_maximizingColumnBasis line 35

theorem OAI.PolycyclicRecognition.det_columnBasis_update line 51

Source documentation

A vector with nonzero coordinate at column j can replace that column. The determinant identity is the exact algebraic exchange witness.

theorem det_columnBasis_update
    (v : I → Fin n → ℝ) (b : Fin n → I) (y : I) (j : Fin n)
    (c : Fin n → ℝ) (hc : ∀ k, v y k = ∑ i, c i * v (b i) k) :
    (columnBasisMatrix v (Function.update b j y)).det =
      c j * (columnBasisMatrix v b).det := by
…

Mentions: OAI.PolycyclicRecognition.columnBasisMatrix

theorem OAI.PolycyclicRecognition.weight_le_of_nonzero_coordinate line 67

Source documentation

Maximal total weight gives domination whenever the coordinate is nonzero.

theorem weight_le_of_nonzero_coordinate
    (v : I → Fin n → ℝ) (w : I → ℝ) (b : Fin n → I)
    (hb : IsMaximizingColumnBasis v w b) (y : I) (j : Fin n)
    (c : Fin n → ℝ) (hc : ∀ k, v y k = ∑ i, c i * v (b i) k)
    (hcj : c j ≠ 0) : w y ≤ w (b j) := by
…

Mentions: OAI.PolycyclicRecognition.IsMaximizingColumnBasis

theorem OAI.PolycyclicRecognition.normalized_coordinate_le line 88

Source documentation

Scaling a maximizing basis introduces no growth in its coordinate coefficients. Zero coordinates require no weight comparison.

theorem normalized_coordinate_le
    (v : I → Fin n → ℝ) (w : I → ℝ) (b : Fin n → I)
    (hb : IsMaximizingColumnBasis v w b) (y : I) (j : Fin n)
    (c : Fin n → ℝ) (hc : ∀ k, v y k = ∑ i, c i * v (b i) k)
    {r : ℝ} (hr : 0 ≤ r) :
    |c j * Real.exp (r * (w y - w (b j)))| ≤ |c j| := by
…

Mentions: OAI.PolycyclicRecognition.IsMaximizingColumnBasis

def OAI.PolycyclicRecognition.columnCoordinates line 104
Source documentation
Coordinates in an invertible selected column basis. The definition also exists for singular selections, which simplifies the finite uniform bound.
```
def columnCoordinates (v : I → Fin n → ℝ) (b : Fin n → I) (y : I) : Fin n → ℝ :=
…
```
theorem OAI.PolycyclicRecognition.columnCoordinates_repr line 107
theorem OAI.PolycyclicRecognition.exists_uniform_normalized_coordinate_bound line 119
Source documentation
A single constant controls every normalized coefficient, uniformly over all weights, all maximizing bases, and all nonnegative scales.
```
theorem exists_uniform_normalized_coordinate_bound [Fintype I]
    (v : I → Fin n → ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (w : I → ℝ) (b : Fin n → I),
      IsMaximizingColumnBasis v w b → ∀ (y : I) (j : Fin n) (r : ℝ), 0 ≤ r →
        |columnCoordinates v b y j * Real.exp (r * (w y - w (b j)))| ≤ C := by
…
```
Mentions: OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.columnCoordinates

theorem OAI.PolycyclicRecognition.scaled_columnCoordinates_repr line 147

Source documentation

The bounded coefficients above reconstruct the scaled vector in the scaled selected basis, exactly as in the weighted box definition.

theorem scaled_columnCoordinates_repr (v : I → Fin n → ℝ) (w : I → ℝ)
    (b : Fin n → I) (hb : (columnBasisMatrix v b).det ≠ 0)
    (y : I) (r : ℝ) (k : Fin n) :
    Real.exp (r * w y) * v y k =
      ∑ i, (columnCoordinates v b y i * Real.exp (r * (w y - w (b i)))) *
        (Real.exp (r * w (b i)) * v (b i) k) := by
…

Mentions: OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.columnCoordinates