NormalizedProbeGenerator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Normalizing the neighboring generator at a contact-facet pivot

theorem OAI.PolycyclicRecognition.normalized_probe_amplitude_le line 12
Source documentation
The original sampling slack and the inward displacement of the pivot add. No fixed positive exponential rate is introduced by normalization.
```
theorem normalized_probe_amplitude_le {t R q c δ r w : ℝ}
    (ht : |t| ≤ R * Real.exp ((1 + δ) * q * r))
    (hw : w = (1 - c * δ) * q * r) :
    |Real.exp (-w) * t| ≤ R * Real.exp (((c + 1) * q) * δ * r) := by
…
```
theorem OAI.PolycyclicRecognition.normalized_probe_generator line 30
Source documentation
Exact normalized logarithm of one of the actual homogeneous generators.
```
theorem normalized_probe_generator (h : H) (i : Fin M.letterCount) (t : ℝ) :
    cartanIdealWeightDilation T H (-h) (t • M.letter i) =
      (Real.exp (-M.weight i h) * t) • M.letter i := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation

theorem OAI.PolycyclicRecognition.normalized_probe_generator_coordinate_le line 40

Source documentation

The bound works in any fixed word-coordinate basis, with its fixed generator norm absorbed into the subexponential radius.

theorem normalized_probe_generator_coordinate_le
    (b : Basis J ℝ (cartanRootIdeal H)) (h : H) (i : Fin M.letterCount)
    {t R q c δ r : ℝ}
    (ht : |t| ≤ R * Real.exp ((1 + δ) * q * r))
    (hh : M.weight i h = (1 - c * δ) * q * r) :
    ‖b.equivFun (cartanIdealWeightDilation T H (-h) (t • M.letter i))‖ ≤
      (R * ‖b.equivFun (M.letter i)‖) * Real.exp (((c + 1) * q) * δ * r) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealWeightDilation