CharacterFullPrimeCells.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The original signed product law from its word and nonword prime cells

def OAI.Ostmann.characterFullPrimeCells line 12

Source documentation

Both signs use the same marginal. Signs change the characters, never the original positive harmonic measure.

noncomputable def characterFullPrimeCells {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f : ℕ)
    (Q : Fin (m + 1) → Finset ℕ)
    (R : (v : CharacterCell k) → Fin (characterCellSize r f v) → Finset ℕ) :
    (Σ v, Fin (characterSize m r f v)) → Finset ℕ
  | ⟨(_, none), i⟩ => Q i
  | ⟨(_, some v), i⟩ => R v i

Mentions: OAI.Ostmann.CharacterCell, OAI.Ostmann.characterCellSize, OAI.Ostmann.characterSize

theorem OAI.Ostmann.characterFullPrimeCells_bulk line 19
theorem OAI.Ostmann.characterFullPrimeCells_top line 24
theorem OAI.Ostmann.characterFullPrimeCells_anchor line 29
theorem OAI.Ostmann.characterFullPrimeCells_subset line 36
theorem OAI.Ostmann.characterFullPrimeCells_mass line 46

theorem OAI.Ostmann.characterFullPrimeCells_source line 59

Source documentation

This equality identifies the literal scheduled law with the two copies of the original word followed by the flattened nonword cells.

theorem characterFullPrimeCells_source {k : ℕ} (m nc : ℕ) (r : Fin k → ℕ) (f : ℕ)
    (cell : (Σ v, Fin (characterCellSize r f v)) ≃ Fin nc)
    (Q : Fin (m + 1) → Finset ℕ)
    (R : (v : CharacterCell k) → Fin (characterCellSize r f v) → Finset ℕ)
    (i : Σ v, Fin (characterSize m r f v)) :
    Fin.append
      (Fin.append Q (fun j => R (cell.symm j).1 (cell.symm j).2))
      (Fin.append Q (fun j => R (cell.symm j).1 (cell.symm j).2))
      (initialWordTupleEquiv (m + 1) nc (characterCellSize r f) cell i) =
        characterFullPrimeCells m r f Q R i := by
…

Mentions: OAI.Ostmann.characterCellSize, OAI.Ostmann.CharacterCell, OAI.Ostmann.characterSize, OAI.Ostmann.initialWordTupleEquiv, OAI.Ostmann.characterFullPrimeCells

theorem OAI.Ostmann.characterFullPrimeCells_probability line 93