TransferHistoryEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Summed square energy without a history multiplicity loss

theorem OAI.Ostmann.transfer_history_energy_eq line 13

Source documentation

Unique histories allow the sum over root-frequency squares to be exchanged exactly for the sum of individual squared coefficients.

theorem transfer_history_energy_eq {State : Type*} (sys : TransferHistorySystem State)
    (n : ℕ) (σ : State) (T : Finset (FrequencyTree ℤ n)) (S : Finset ℤ)
    (hS : ∀ x ∈ T, ValidTransferHistory sys n σ x → frequencyRoot n x ∈ S)
    (c : FrequencyTree ℤ n → ℂ) :
    (∑ s ∈ S, ‖∑ x ∈ historiesAtRoot sys n σ T s, c x‖ ^ 2) =
      ∑ x ∈ T, if ValidTransferHistory sys n σ x then ‖c x‖ ^ 2 else 0 := by
…

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

theorem OAI.Ostmann.transfer_history_phase_energy_le line 32

Source documentation

The graph phase is discarded only after the unique-history square is formed. This is the original squared-weight majorant in the manuscript.

theorem transfer_history_phase_energy_le {State : Type*} (sys : TransferHistorySystem State)
    (n : ℕ) (σ : State) (T : Finset (FrequencyTree ℤ n)) (S : Finset ℤ)
    (hS : ∀ x ∈ T, ValidTransferHistory sys n σ x → frequencyRoot n x ∈ S)
    (W Θ : FrequencyTree ℤ n → ℂ)
    (hΘ : ∀ x ∈ T, ValidTransferHistory sys n σ x → ‖Θ x‖ ≤ 1) :
    (∑ s ∈ S, ‖∑ x ∈ historiesAtRoot sys n σ T s, W x * Θ x‖ ^ 2) ≤
      ∑ x ∈ T, if ValidTransferHistory sys n σ x then ‖W x‖ ^ 2 else 0 := by
…

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