OAI/NumberTheory/Ostmann/Construction/ScheduledFinalComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledPrimePrior line 12
2. theorem OAI.Ostmann.scheduledPrimePrior_preserved line 17
3. theorem OAI.Ostmann.scheduledFullSamplePerm_energy line 25
4. theorem OAI.Ostmann.scheduledPrimePrior_mass line 36
5. theorem OAI.Ostmann.scheduled_full_final_comparison line 44

   Source documentation

   The diagonal energy is unchanged, and only distinct final pairs require cancellation. The law is the full original product measure on surviving slots.

   theorem scheduled_full_final_comparison {I A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (n m : ℕ)
       (word : Fin m ≃ {i : I // role i = .word})
       (μ : I → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hμmass : ∀ i, ∑ a, μ i a = 1)
       (F : (CopyScheduleAtoms role (n + 1) → A) → ℂ) (B E : ℝ) (hE : 0 ≤ E)
       (henergy : ∑ x, scheduledPrimePrior role (n + 1) μ x * ‖F x‖ ^ 2 ≤ B)
       (hpair : ∀ e f : FinalParityReassignments n m, e ≠ f →
         ‖∑ x, (scheduledPrimePrior role (n + 1) μ x : ℂ) *
           (F (scheduledFullSamplePerm role n m word e x) *
             star (F (scheduledFullSamplePerm role n m word f x)))‖ ≤ E) :
       ‖∑ x, (scheduledPrimePrior role (n + 1) μ x : ℂ) * F x‖ ^ 2 ≤
         B / (((Nat.factorial (2 ^ n)) ^ 2) ^ m : ℕ) + E := by
   …

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

6. theorem OAI.Ostmann.scheduled_root_final_comparison line 74

   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 scheduled_root_final_comparison {I A R : Type*}
       [Fintype I] [Fintype A] [Fintype R]
       (role : I → CopyScheduleRole) (n m : ℕ)
       (word : Fin m ≃ {i : I // role 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 (scheduledFullSamplePerm role n m word e x) *
             star (F s (scheduledFullSamplePerm role n m word 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.scheduledFullSamplePerm