OAI/NumberTheory/Ostmann/Construction/WeightedWordLeaves.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The literal frequency and polynomial of every reconstructed Fourier leaf

  1. structure OAI.Ostmann.WeightedWordLeaf line 11
  2. def OAI.Ostmann.WeightedWordLeaf.flip line 18
  3. def OAI.Ostmann.WeightedWordLeaf.toSignedFormula line 21
  4. def OAI.Ostmann.WeightedWordLeaf.evaluate line 24
  5. def OAI.Ostmann.WordTransferTemplate.weightedLeaves line 29
  6. theorem OAI.Ostmann.weightedWordLeaf_flip_projection line 38
  7. theorem OAI.Ostmann.WordTransferTemplate.weightedLeaves_projection line 44
  8. theorem OAI.Ostmann.WordTransferTemplate.weightedLeaves_length line 55
  9. def OAI.Ostmann.evaluatedTransferLeaf line 64

    Source documentation

    Preserve the actual leaf frequency as well as its sign and word value.

    noncomputable def evaluatedTransferLeaf {σ : Type*}
    (z : (WordTransferState σ × ℤ) × Bool) : Bool × ℤ × ℚ :=
…

    Mentions: OAI.Ostmann.WordTransferState

  10. def OAI.Ostmann.flipEvaluatedLeaf line 68
  11. theorem OAI.Ostmann.weightedWordLeaf_flip_evaluate line 70
  12. theorem OAI.Ostmann.evaluatedTransferLeaf_flip line 76
  13. theorem OAI.Ostmann.WordTransferTemplate.weightedLeaves_value line 82