OAI/Topology/ArtinGroups/ParabolicIntersections/MeshProjectionInduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Jones--Wenzl induction before the first nonpositive quantum integer.

  1. structure OAI.HarmonicArtin.ParabolicIntersections.MeshProjectionStage line 10
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjectionStage_zero line 26
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjectionStage_succ line 43
  4. theorem OAI.HarmonicArtin.ParabolicIntersections.meshProjectionStage_before_cutoff line 91

    Source documentation

    Every stage strictly before the quantum cutoff is an actual orthogonal projection, with the required nesting and scalar identity.

    theorem meshProjectionStage_before_cutoff (μ : 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+1<H → MeshProjectionStage G μ δ n := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshQuantum, OAI.HarmonicArtin.ParabolicIntersections.MeshProjectionStage