MeshProjectionCutoff.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual path projections vanish at a finite quantum cutoff.

lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_trace_zero line 10
lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_trace_one line 15
lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_trace_step line 24
theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjection_weightedTrace line 47
Source documentation
The weighted trace is the quantum integer, without any graph classification or assumption of mesh nilpotence.
```
theorem meshProjection_weightedTrace (μ : V → ℝ) (hμ : ∀ v, 0<μ v) (δ : ℝ)
    (heigen : ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=δ*μ v)
    (H : ℕ) (hpos : ∀ n, 0 < n → n < H → 0 < meshQuantum δ n) :
    ∀ n, n<H → meshWeightedTrace μ (meshProjection G μ δ n)=
      (meshQuantum δ (n+1) : ℂ)*∑ v, (μ v : ℂ) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshQuantum, OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace, OAI.HarmonicArtin.ParabolicIntersections.meshProjection
theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjection_eventually_zero line 74
Source documentation
Some positive length has zero path projection. This is the finite essential-path bound, proved from a positive adjacency eigenvector below 2.
```
theorem meshProjection_eventually_zero (μ : V → ℝ) (hμ : ∀ v, 0<μ v)
    (δ : ℝ) (hδ0 : 0<δ) (hδ2 : δ<2)
    (heigen : ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=δ*μ v) :
    ∃ N : ℕ, 0<N ∧ ∀ v, meshProjection G μ δ N v=0 := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshProjection