OAI/NumberTheory/Ostmann/Construction/ConstituentMatchingEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primePermutationCorrelation_split line 12
2. theorem OAI.Ostmann.constituent_matching_energy_bound line 31

   Source documentation

   This holds for every matching, including the bad component-rich ones. Its small factor is the exact counterpart harmonic normalizer and product lower endpoint. The retained square has its original H prime law.

   theorem constituent_matching_energy_bound {I D R : Type*}
       [Fintype I] [Fintype D] [Fintype R]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (χ : (Σ i, Fin (size i)) → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : (Σ i, Fin (size i)) → ℕ → ℂ) (pivot : ℕ → (Σ i, Fin (size i)))
       (hκ : ∀ i p, ‖κ i p‖ ≤ 1)
       (n : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → FrequencyTree ℤ n)
       (hhist : Function.Injective hist) (root : D → R)
       (hroot : ∀ d d', root d = root d' → frequencyRoot n (hist d) = frequencyRoot n (hist d'))
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → P) (M : ℕ)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyRoot, OAI.Ostmann.CopyScheduleY