CharacterRounding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integer rounding in the detecting-character argument

The character used at a matrix size may depend on that size. A uniform bound on all those characters is enough: the loss of one in rounding their target values cannot change a positive power exponent. The character-existence and character-growth assumptions remain explicit in the final implications.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nat_sub_one_le_lt line 22
Source documentation
Rounding strictly down works at integers too: use ceil x - 1.
```
theorem exists_nat_sub_one_le_lt {x : ℝ} (hx : 0 < x) :
    ∃ k : ℕ, x - 1 ≤ (k : ℝ) ∧ (k : ℝ) < x := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.rpow_exponent_le_of_nat_sub_one_bound line 33
Source documentation
An additive loss of one does not affect a comparison to a nonnegative power exponent. No sign assumption on the exponent on the left is needed.
```
theorem rpow_exponent_le_of_nat_sub_one_bound {ν τ : ℝ} (hτ : 0 ≤ τ)
    (hbound : ∀ d : ℕ, 2 ≤ d → (d : ℝ) ^ ν - 1 ≤ (d : ℝ) ^ τ) :
    ν ≤ τ := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_integer_rounding line 47

Source documentation

The integer witnesses in the final rounding argument can vary with d.

theorem exponent_le_of_integer_rounding {ν τ : ℝ} (hτ : 0 ≤ τ)
    (hround : ∀ d : ℕ, 2 ≤ d →
      ∃ k : ℕ, (d : ℝ) ^ ν - 1 ≤ k ∧ (k : ℝ) ≤ (d : ℝ) ^ τ) :
    ν ≤ τ := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_integer_rounding_of_pos line 58
Source documentation
A positive exponent on the left makes the target exponent nonnegative automatically, so it is an alternative to that hypothesis above.
```
theorem exponent_le_of_integer_rounding_of_pos {ν τ : ℝ} (hν : 0 < ν)
    (hround : ∀ d : ℕ, 2 ≤ d →
      ∃ k : ℕ, (d : ℝ) ^ ν - 1 ≤ k ∧ (k : ℝ) ≤ (d : ℝ) ^ τ) :
    ν ≤ τ := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_detecting_characters line 79

Source documentation

Explicitly conditional passage from detecting characters to the exponent bound. The detecting character is allowed to depend on both d and k.

theorem exponent_le_of_detecting_characters {ν τ : ℝ} (hτ : 0 ≤ τ)
    (detect : ∀ d : ℕ, 2 ≤ d → ∀ k : ℕ, (k : ℝ) < (d : ℝ) ^ ν →
      ∃ χ : Character, (k : ℝ) ≤ χ.value (Tensor.matrixMultiplication d d d))
    (bound : ∀ χ : Character, ∀ d : ℕ, 2 ≤ d →
      χ.value (Tensor.matrixMultiplication d d d) ≤ (d : ℝ) ^ τ) :
    ν ≤ τ := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exponent_le_of_detecting_character_exponents line 95

Source documentation

The character growth bound can be supplied as a uniform bound on its exponent sum, together with the matrix-value identity.

theorem exponent_le_of_detecting_character_exponents {ν τ : ℝ} (hτ : 0 ≤ τ)
    (exponentSum : Character → ℝ)
    (value : ∀ χ : Character, ∀ d : ℕ, 2 ≤ d →
      χ.value (Tensor.matrixMultiplication d d d) = (d : ℝ) ^ exponentSum χ)
    (upper : ∀ χ : Character, exponentSum χ ≤ τ)
    (detect : ∀ d : ℕ, 2 ≤ d → ∀ k : ℕ, (k : ℝ) < (d : ℝ) ^ ν →
      ∃ χ : Character, (k : ℝ) ≤ χ.value (Tensor.matrixMultiplication d d d)) :
    ν ≤ τ := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent_le_nine_quarters_of_characters line 111

Source documentation

The paper's final ν ≤ 9/4 implication, with its two substantive character inputs visible rather than incorporated into the definition of ν.

theorem exactRankExponent_le_nine_quarters_of_characters
    (detect : ∀ d : ℕ, 2 ≤ d → ∀ k : ℕ,
      (k : ℝ) < (d : ℝ) ^ exactRankExponent →
      ∃ χ : Character, (k : ℝ) ≤ χ.value (Tensor.matrixMultiplication d d d))
    (bound : ∀ χ : Character, ∀ d : ℕ, 2 ≤ d →
      χ.value (Tensor.matrixMultiplication d d d) ≤ (d : ℝ) ^ (9 / 4 : ℝ)) :
    exactRankExponent ≤ 9 / 4 :=
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRankExponent, OAI.MatrixMultiplication.AuxiliarySeparation.Character