OAI/NumberTheory/Ostmann/Construction/FinalHistoryCorrelations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finalHistorySum line 13
2. theorem OAI.Ostmann.final_history_energy line 20

   Source documentation

   Root counting measure and the original assignment prior are retained. History uniqueness removes cross terms before taking any absolute bounds.

   theorem final_history_energy {X State : Type*} [Fintype X]
       (sys : TransferHistorySystem State) (n : ℕ) (state : X → State)
       (T : Finset (FrequencyTree ℤ n)) (S : Finset ℤ) (μ : X → ℝ)
       (hμ : ∀ x, 0 ≤ μ x) (W Θ : X → FrequencyTree ℤ n → ℂ)
       (hS : ∀ x h, h ∈ T → ValidTransferHistory sys n (state x) h → frequencyRoot n h ∈ S)
       (hΘ : ∀ x h, h ∈ T → ValidTransferHistory sys n (state x) h → ‖Θ x h‖ ≤ 1) :
       (∑ s ∈ S, ∑ x, μ x * ‖finalHistorySum sys n (state x) T s (W x) (Θ x)‖ ^ 2) ≤
         ∑ x, μ x * ∑ h ∈ T, if ValidTransferHistory sys n (state x) h then ‖W x h‖ ^ 2 else 0 := by
   …

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

3. theorem OAI.Ostmann.finite_history_pair_expansion line 37

   Source documentation

   Each term carries its own sharp support, including its root-frequency condition. This identity is used before applying the one-sided estimate.

   theorem finite_history_pair_expansion {X H K : Type*} [Fintype X]
       (μ : X → ℝ) (T : Finset H) (U : Finset K) (a : H → X → ℂ) (b : K → X → ℂ) :
       (∑ x, (μ x : ℂ) * ((∑ h ∈ T, a h x) * conj (∑ k ∈ U, b k x))) =
         ∑ h ∈ T, ∑ k ∈ U, ∑ x, (μ x : ℂ) * (a h x * conj (b k x)) := by
   …

4. theorem OAI.Ostmann.finite_history_pair_bound line 52

   Source documentation

   The cost of fixing both finite-depth frequency histories is recorded explicitly. All arithmetic and coprimality guards stay in the term functions.

   theorem finite_history_pair_bound {X H K : Type*} [Fintype X]
       (μ : X → ℝ) (T : Finset H) (U : Finset K) (a : H → X → ℂ) (b : K → X → ℂ)
       (E : ℝ) (hpair : ∀ h ∈ T, ∀ k ∈ U,
         ‖∑ x, (μ x : ℂ) * (a h x * conj (b k x))‖ ≤ E) :
       ‖∑ x, (μ x : ℂ) * ((∑ h ∈ T, a h x) * conj (∑ k ∈ U, b k x))‖ ≤
         (T.card : ℝ) * U.card * E := by
   …

5. theorem OAI.Ostmann.diagonal_pair_eq_energy line 68

   Source documentation

   A same-function pair is precisely the nonnegative diagonal energy.

   theorem diagonal_pair_eq_energy {X : Type*} [Fintype X]
       (μ : X → ℝ) (hμ : ∀ x, 0 ≤ μ x) (A : X → ℂ) :
       ‖∑ x, (μ x : ℂ) * (A x * conj (A x))‖ = ∑ x, μ x * ‖A x‖ ^ 2 := by
   …