MeshProjectionAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional projection calculation in the mesh argument.

theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_scalar_step line 13

Source documentation

The loop, adjacent, and prefix identities give the next scalar in the projection recurrence.

theorem mesh_scalar_step (C D : Matrix I J ℂ) (P : Matrix I I ℂ)
    (R : Matrix J J ℂ) (delta a : ℂ)
    (hPsq : P*P=P) (hCR : C*R=P*C) (hRC : R*C.conjTranspose=C.conjTranspose*P)
    (hloop : C*C.conjTranspose=delta • (1 : Matrix I I ℂ))
    (hadj : C*D.conjTranspose=1) (hadj' : D*C.conjTranspose=1) :
    C*(R-a • (R*D.conjTranspose*D*R))*C.conjTranspose=(delta-a) • P := by
…

theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_projection_correction line 33

Source documentation

Removing the scaled row-space projection imposes one more contraction. All hypotheses here are matrix identities, proved for the path operators in the mesh construction.

theorem mesh_projection_correction (Q : Matrix I I ℂ) (T : Matrix J I ℂ)
    (P : Matrix J J ℂ) (lam : ℝ) (hlam : lam≠0)
    (hQstar : Q.conjTranspose=Q) (hQsq : Q*Q=Q)
    (hTQ : T*Q=T) (hTT : T*T.conjTranspose=(lam : ℂ) • P) (hPT : P*T=T) :
    let R := Q - ((lam⁻¹ : ℝ) : ℂ) • (T.conjTranspose*T)
…

theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_projection_trace line 81
Source documentation
A self-adjoint idempotent is positive, and trace zero forces it to vanish. These are the positivity facts used at the scalar cutoff.
```
theorem mesh_projection_trace (P : Matrix I I ℂ)
    (hstar : P.conjTranspose=P) (hsq : P*P=P) :
    0≤(Matrix.trace P).re ∧ (Matrix.trace P=0 ↔ P=0) := by
…
```