OAI/NumberTheory/Ostmann/Arithmetic/FrequencyBulkSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.treeIntegerResidues_of_naturalLift line 13
2. theorem OAI.Ostmann.bulkUnitRepresentative_coprime line 21
3. theorem OAI.Ostmann.frequencyModelBulkCore_norm_support line 39

   Source documentation

   Keep the support indicator while taking the norm of the actual core. The adaptive data uses the fixed nonbulk values; only the bulk law varies.

   theorem frequencyModelBulkCore_norm_support {σ : Type*}
       (base : σ → ℕ) (tier : σ → ℕ) (S : Finset ℤ) (n m R : ℕ)
       [NeZero (R ^ (n - 1 + 2))] (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0) (hR : ∀ b (j : Fin (2 ^ n - 1)),
       (singleTreeNodeFrequencies S n (frequencyPairProjection S n b t) j.val).root.natAbs ∣ R)
       (slot : (TreeLeafIndex n × Fin m) ↪ σ)
       (small : Bool → TreeLeafTuple (List σ) n) (a : Bool → MovingSampleSlots σ n)
       (hslot : ∀ j, n ≤ tier (slot j))
       (hsmall : ∀ b i, i ∈ flattenMovingSlots n (small b) → i ∉ Set.range slot)
       (ha : ∀ b, (a b).Levels tier)
       (hbase : ∀ i ∉ Set.range slot, IsCoprime (base i : ℤ) (R : ℤ))
       (F : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℂ)
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.frequencyPairProjection, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.MovingSlotData

4. theorem OAI.Ostmann.arithmeticLeafSupport_bulk_average line 87

   Source documentation

   Passing from individual bulk slots to their leaf products is an exact uniform averaging identity.

   theorem arithmeticLeafSupport_bulk_average {Q : ℕ} [NeZero Q] (n m : ℕ) (hm : 0 < m)
       (data : (ZMod Q)ˣ → List (ZMod Q)ˣ → Option (ArithmeticSplitData Q × ArithmeticSplitData Q)) :
       (Fintype.card (TreeLeafIndex n × Fin m → (ZMod Q)ˣ) : ℝ)⁻¹ *
         (∑ z : TreeLeafIndex n × Fin m → (ZMod Q)ˣ, arithmeticLeafSupport n data
           ((treeLeafTupleEquiv (ZMod Q)ˣ n).symm (bulkBlockProduct z))) =
         (Fintype.card (TreeLeafTuple (ZMod Q)ˣ n) : ℝ)⁻¹ *
           ∑ z : TreeLeafTuple (ZMod Q)ˣ n, arithmeticLeafSupport n data z := by
   …

   Mentions: OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.arithmeticLeafSupport, OAI.Ostmann.treeLeafTupleEquiv, OAI.Ostmann.bulkBlockProduct, OAI.Ostmann.TreeLeafTuple