ActiveColors.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Active colors for a relative frame

Section 6.3 of paper 082-03 requires an active-color argument without universal adjacency of the frame. Null signs are allowed at every recorded level, including the cutoff. All assertions here are proved from the Cartan matrix and the finite profile.

def OAI.HarmonicArtin.ParabolicIntersections.relativePositiveSign line 21
Source documentation
A closed positive null component, isolated from all higher levels.
```
def relativePositiveSign (C : Matrix ι ι ℝ) (U : Set ι)
    (p : ℕ →₀ (ι → ℝ)) (k : ℕ) (i : ι) : Prop :=
…
```
def OAI.HarmonicArtin.ParabolicIntersections.relativeActive line 28
Source documentation
Active colors at their last recorded incidence.
```
def relativeActive (C : Matrix ι ι ℝ) (U : Set ι)
    (p : ℕ →₀ (ι → ℝ)) (i : ι) : Prop :=
…
```

theorem OAI.HarmonicArtin.ParabolicIntersections.relative_active_component_posDef line 36

Source documentation

Every connected component formed from a positive definite closed part and active colors remains positive definite.

theorem relative_active_component_posDef
    (C : Matrix ι ι ℝ) (hSym : ∀ i j, C i j = C j i)
    (hOff : ∀ i j, i ≠ j → C i j ≤ 0) (U : Set ι)
    (p : ℕ →₀ (ι → ℝ)) (hp : ∀ k i, 0 ≤ p k i)
    (T : Set ι) (hT : (C.submatrix Subtype.val Subtype.val : Matrix T T ℝ).PosDef)
    (hHarm : ∀ k, ∀ i ∈ T, (C *ᵥ p k) i = 0)
    (G : Set ι) (hU : G ⊆ U)
    (hG : ∀ i ∈ G, i ∈ T ∨ relativeActive C U p i)
    (hConn : ∀ i j : G, Relation.ReflTransGen (fun a b : G => C a b < 0) i j) :
    (C.submatrix Subtype.val Subtype.val : Matrix G G ℝ).PosDef := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.relativeActive

theorem OAI.HarmonicArtin.ParabolicIntersections.relative_active_posDef line 140