OAI/NumberTheory/Ostmann/Construction/FullAtomTransferWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.fullAtomWeightGuard line 11
2. def OAI.Ostmann.fullAtomTransferWeight line 19
3. def OAI.Ostmann.fullAtomRootGuard line 28
4. theorem OAI.Ostmann.fullAtomWeightGuard_node line 34
5. theorem OAI.Ostmann.guarded_product line 48
6. theorem OAI.Ostmann.fullAtomTransferWeight_node line 55

   Source documentation

   The full weight has exactly the inherited left/right factors, with all new top tests in the root guard. There is no loss of boundary or unit tests.

   theorem fullAtomTransferWeight_node {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (n : ℕ)
       (x : CopyScheduleAtoms role (n + 1) → ℕ) (t : FrequencyTree ℤ (n + 1)) (P : ℕ)
       (hP : ValidTransferNode (scheduleAtomSystem role childBound pivotBound) ⟨n + 1, x⟩
         t.1 (frequencyRoot n t.2.1) (frequencyRoot n t.2.2) P) :
       fullAtomTransferWeight role childBound pivotBound ranges leaf (n + 1) x t =
         if fullAtomRootGuard role ranges n x P t.1 then
           fullAtomTransferWeight role childBound pivotBound ranges leaf n
             (reverseCopyLabelMap role n true P x) t.2.1 *
           conj (fullAtomTransferWeight role childBound pivotBound ranges leaf n
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.frequencyRoot, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.fullAtomRootGuard, OAI.Ostmann.reverseCopyLabelMap

7. theorem OAI.Ostmann.groupedFullCoprimeFourierWeight_atom line 75

   Source documentation

   Evaluation at arbitrary words is just evaluation at their atom products.

   theorem groupedFullCoprimeFourierWeight_atom {I V : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (n : ℕ) (words : CopyScheduleAtoms role n → List V)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (t : FrequencyTree ℤ n) (q : V → ℕ) :
       groupedFullCoprimeFourierWeight role n words childBound pivotBound ranges ψ X lo hi t q =
         fullAtomTransferWeight role childBound pivotBound ranges
           (fun τ v => (if (scheduleAtomTotal role τ : ℝ) / X ∈ Set.Icc lo hi then (1 : ℂ) else 0) *
             normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v ((scheduleAtomTotal role τ : ℝ) / X))
           n (fun i => ((words i).map q).prod) t := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.groupedFullCoprimeFourierWeight, OAI.Ostmann.fullAtomTransferWeight, OAI.Ostmann.scheduleAtomTotal, OAI.Ostmann.normalizedFourierProfile