OAI/NumberTheory/Ostmann/Construction/SelectedFinalComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.selectedPrimePrior_preserved line 10
2. theorem OAI.Ostmann.selectedFullSamplePerm_energy line 18
3. theorem OAI.Ostmann.selected_full_final_comparison line 29
4. theorem OAI.Ostmann.selected_root_final_comparison line 59

   Source documentation

   The manuscript's measure includes a shared root frequency. Reassignments act only on the prime coordinates, so the root is identical in every pair.

   theorem selected_root_final_comparison {I A R : Type*}
       [Fintype I] [Fintype A] [Fintype R]
       (role : I → CopyScheduleRole) (n m : ℕ)
       (bulk : Fin m ↪ I) (hbulk : ∀ i, role (bulk i) = .word)
       (μ : I → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hμmass : ∀ i, ∑ a, μ i a = 1)
       (F : R → (CopyScheduleAtoms role (n + 1) → A) → ℂ) (B E : ℝ) (hE : 0 ≤ E)
       (henergy : ∑ s, ∑ x, scheduledPrimePrior role (n + 1) μ x * ‖F s x‖ ^ 2 ≤ B)
       (hpair : ∀ e f : FinalParityReassignments n m, e ≠ f →
         ‖∑ s, ∑ x, (scheduledPrimePrior role (n + 1) μ x : ℂ) *
           (F s (selectedFullSamplePerm role n m bulk hbulk e x) *
             star (F s (selectedFullSamplePerm role n m bulk hbulk f x)))‖ ≤ E) :
       ‖∑ s, ∑ x, (scheduledPrimePrior role (n + 1) μ x : ℂ) * F s x‖ ^ 2 ≤
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduledPrimePrior, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.selectedFullSamplePerm