OAI/NumberTheory/Ostmann/Construction/TransferHistorySquare.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.historiesAtRoot line 12
2. theorem OAI.Ostmann.historiesAtRoot_card_le_one line 17
3. theorem OAI.Ostmann.history_root_square_eq line 28

   Source documentation

   The exact square identity uses uniqueness before any averaging or coefficient majorization. It applies equally to a fixed external pivot state.

   theorem history_root_square_eq {State : Type*} (sys : TransferHistorySystem State)
       (n : ℕ) (σ : State) (T : Finset (FrequencyTree ℤ n)) (s : ℤ)
       (c : FrequencyTree ℤ n → ℂ) :
       ‖∑ x ∈ historiesAtRoot sys n σ T s, c x‖ ^ 2 =
         ∑ x ∈ historiesAtRoot sys n σ T s, ‖c x‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.historiesAtRoot