OAI/NumberTheory/Ostmann/Construction/SpectatorWeightFactorization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.recursiveTransferWeight_mul_leaf line 11
2. theorem OAI.Ostmann.copyScheduleSurvives_outside line 27
3. def OAI.Ostmann.persistentSpectatorAtom line 35
4. theorem OAI.Ostmann.persistentSpectatorAtom_reverse line 39
5. theorem OAI.Ostmann.coprime_spectator_cast_ne_zero line 50
6. theorem OAI.Ostmann.full_support_spectator_cutoff line 61

   Source documentation

   The outside prime is unchanged along both branches. Every original coprimality guard therefore forces the spectator zero convention to pass.

   theorem full_support_spectator_cutoff {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (i : I) (hi : role i = .outside) {q : ℕ} [Fact q.Prime]
       (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (t : FrequencyTree ℤ n)
       (hq : x (persistentSpectatorAtom role i hi n) = q)
       (hc : scheduleAtomFullCoprimeValid role childBound pivotBound n x t)
       (G : ScheduleAtomState role → ℤ → ℂ) :
       recursiveTransferWeight (scheduleAtomSystem role childBound pivotBound) G
         (spectatorHistoryCutoff (q := q) (scheduleAtomSystem role childBound pivotBound)) n ⟨n, x⟩ t =
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.persistentSpectatorAtom, OAI.Ostmann.scheduleAtomFullCoprimeValid, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.spectatorHistoryCutoff

7. theorem OAI.Ostmann.fullAtomTransferWeight_spectator_factor line 99
8. theorem OAI.Ostmann.fullAtomTransferWeight_mul_leaf line 119
9. theorem OAI.Ostmann.fullAtomTransferWeight_prod_leaf line 134
10. theorem OAI.Ostmann.fullAtomTransferWeight_spectator_tree line 156