MeshQuantum.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite positivity interval for the Jones--Wenzl scalar recurrence.

def OAI.HarmonicArtin.ParabolicIntersections.meshQuantum line 9
Source documentation
Quantum integers as a real recurrence, with no trigonometric choices.
```
noncomputable def meshQuantum (δ : ℝ) : ℕ → ℝ
  | 0 => 0
  | 1 => 1
  | n+2 => δ*meshQuantum δ (n+1)-meshQuantum δ n
```
lemma OAI.HarmonicArtin.ParabolicIntersections.meshQuantum_zero line 14
lemma OAI.HarmonicArtin.ParabolicIntersections.meshQuantum_one line 15
lemma OAI.HarmonicArtin.ParabolicIntersections.meshQuantum_step line 16
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_quantum_eventually_nonpositive line 21
Source documentation
For δ<2, the recurrence starting at 0,1 cannot remain strictly positive. This discrete concavity proof avoids choosing an angle.
```
theorem mesh_quantum_eventually_nonpositive (δ : ℝ) (hδ : δ<2)
    (q : ℕ → ℝ) (hzero : q 0=0) (hone : q 1=1)
    (hrec : ∀ n, q (n+2)=δ*q (n+1)-q n) :
    ∃ n, 0<n ∧ q n≤0 := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_quantum_cutoff line 92
Source documentation
The first nonpositive scalar gives a finite cutoff, and all earlier nonzero-index scalars are positive, as required by the projection recursion.
```
theorem mesh_quantum_cutoff (δ : ℝ) (hδ0 : 0<δ) (hδ2 : δ<2)
    (q : ℕ → ℝ) (hzero : q 0=0) (hone : q 1=1)
    (hrec : ∀ n, q (n+2)=δ*q (n+1)-q n) :
    ∃ h, 3≤h ∧ q h≤0 ∧ ∀ n, 0<n → n<h → 0<q n := by
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.meshQuantum_cutoff line 113
lemma OAI.HarmonicArtin.ParabolicIntersections.meshQuantum_ratio_step line 119