OAI/NumberTheory/Ostmann/Arithmetic/RecursiveSupportExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.transferNodeCutoff line 11
2. def OAI.Ostmann.transferLeafCutoff line 15
3. theorem OAI.Ostmann.transferLeafCutoff_flip line 19
4. theorem OAI.Ostmann.recursiveSupportFactor_product line 28

   Source documentation

   The support is exactly the product of original node and leaf cutoffs on the original arithmetic validity set.

   theorem recursiveSupportFactor_product {State : Type*}
       (sys : TransferHistorySystem State) (leafCutoff : State → ℤ → ℝ)
       (cutoff : State → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
       recursiveSupportFactor sys leafCutoff cutoff n σ t =
         if ValidTransferHistory sys n σ t then
           ((transferNodeList sys n σ t).map (transferNodeCutoff cutoff)).prod *
             ((transferLeafList sys n σ t).map (transferLeafCutoff leafCutoff)).prod
         else 0 := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveSupportFactor, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.transferNodeList, OAI.Ostmann.transferNodeCutoff, OAI.Ostmann.transferLeafList, OAI.Ostmann.transferLeafCutoff

5. theorem OAI.Ostmann.recursiveSupportFactor_nodeList line 50

   Source documentation

   The flat statement uses exactly 2^n-1 node tests, whose validity was proved equivalent to the recursive support, not assumed as a new condition.

   theorem recursiveSupportFactor_nodeList {State : Type*}
       (sys : TransferHistorySystem State) (leafCutoff : State → ℤ → ℝ)
       (cutoff : State → ℤ → ℤ → ℤ → ℝ)
       (n : ℕ) (σ : State) (t : FrequencyTree ℤ n) :
       recursiveSupportFactor sys leafCutoff cutoff n σ t =
         if ∀ node ∈ transferNodeList sys n σ t, node.Valid sys then
           ((transferNodeList sys n σ t).map (transferNodeCutoff cutoff)).prod *
             ((transferLeafList sys n σ t).map (transferLeafCutoff leafCutoff)).prod
         else 0 := by
   …

   Mentions: OAI.Ostmann.TransferHistorySystem, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveSupportFactor, OAI.Ostmann.transferNodeList, OAI.Ostmann.transferNodeCutoff, OAI.Ostmann.transferLeafList, OAI.Ostmann.transferLeafCutoff