OAI/Topology/ArtinGroups/ParabolicIntersections/MeshProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ParabolicIntersections.meshProjection line 15

   Source documentation

   The correction formula removes precisely the final contraction from the already projected prefix. Only positive-index quantum integers occur as denominators before the cutoff.

   noncomputable def meshProjection (μ : V → ℝ) (δ : ℝ) :
       (n : ℕ) → (v : V) → Matrix (MeshPaths G n v) (MeshPaths G n v) ℂ
     | 0, _ => 1
     | 1, _ => 1
     | n+2, v =>
       let Q := meshExtendMatrix G (meshProjection μ δ (n+1)) v
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths, OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix

2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_zero line 25
3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_one line 28
4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_step line 31
5. theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjection_selfAdjoint line 40

   Source documentation

   Self-adjointness uses only the real coefficients in the recursion; it holds even beyond the range in which the matrices are projections.

   theorem meshProjection_selfAdjoint (μ : V → ℝ) (δ : ℝ) :
       ∀ n v, (meshProjection G μ δ n v).conjTranspose=meshProjection G μ δ n v := by
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshProjection

6. theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjection_correct line 57

   Source documentation

   One step of the actual recursion, once its scalar identity has been established from the preceding path identities.

   theorem meshProjection_correct (μ : V → ℝ) (δ : ℝ) (n : ℕ) (v : V)
       (hden : meshQuantum δ (n+2)/meshQuantum δ (n+1)≠0)
       (hQstar : (meshExtendMatrix G (meshProjection G μ δ (n+1)) v).conjTranspose=
         meshExtendMatrix G (meshProjection G μ δ (n+1)) v)
       (hQsq : meshExtendMatrix G (meshProjection G μ δ (n+1)) v *
         meshExtendMatrix G (meshProjection G μ δ (n+1)) v=
         meshExtendMatrix G (meshProjection G μ δ (n+1)) v)
       (hscalar : meshContractionMatrix G μ n v *
         meshExtendMatrix G (meshProjection G μ δ (n+1)) v *
         (meshContractionMatrix G μ n v).conjTranspose =
         ((meshQuantum δ (n+2)/meshQuantum δ (n+1) : ℝ) : ℂ) • meshProjection G μ δ n v)
       (himage : meshProjection G μ δ n v * (meshContractionMatrix G μ n v *
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshQuantum, OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix, OAI.HarmonicArtin.ParabolicIntersections.meshProjection, OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix

7. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_extend_step line 108
8. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_scalar_zero line 127
9. lemma OAI.HarmonicArtin.ParabolicIntersections.meshProjection_scalar_succ line 139