MovingRecursiveSupport.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Full original support as local guards in the sampled recursion

All current-state coprimalities and all descendant-frequency unit tests are retained. This puts the existing fully supported coefficient into the local recursion form, without conditioning any internal sample prior.

def OAI.Ostmann.movingLocalSupport line 16
def OAI.Ostmann.movingGuardedLeaf line 21
def OAI.Ostmann.movingGuardedExtra line 25
theorem OAI.Ostmann.movingFullSupport_node line 30
theorem OAI.Ostmann.movingSlotCutoff_guarded line 40

theorem OAI.Ostmann.movingSupportedWeight_recursive line 51

Source documentation

The fully supported original history coefficient equals the recursive coefficient with the literal local support test at each node and leaf.

theorem movingSupportedWeight_recursive {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
    (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (XL XR : ℕ) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
      (movingGuardedLeaf value outside F)
      (movingSlotCutoff value childBound pivotBound (movingGuardedExtra value outside E))
      n ⟨n, T, XL, XR⟩ t =
        movingSupportedWeight value outside T XL XR
          (recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
            (movingSlotCutoff value childBound pivotBound E) n ⟨n, T, XL, XR⟩ t) := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingGuardedLeaf, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingGuardedExtra, OAI.Ostmann.movingSupportedWeight

theorem OAI.Ostmann.movingFrequencySkeleton_frequencyTree line 111
theorem OAI.Ostmann.MovingSlotData.skeleton_frequencyProduct line 120
theorem OAI.Ostmann.MovingSlotData.rootData_regularSlots line 128
theorem OAI.Ostmann.MovingSlotData.rootData_frequencyProduct line 132
theorem OAI.Ostmann.MovingSlotData.rootData_idempotent line 139
theorem OAI.Ostmann.movingLocalSupport_rootData line 146
theorem OAI.Ostmann.movingLocalExtra_guarded line 153

theorem OAI.Ostmann.movingSampledWeight_supported line 163

Source documentation

The sample expansion of the fully supported original coefficient. Every sample retains its original weight, including samples whose support fails.

theorem movingSampledWeight_supported {σ : Type*} [Fintype σ] (value : σ → ℕ)
    (outside : List ℕ) (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (XL XR : ℕ) :
    movingSampledWeight value μ childBound pivotBound (movingGuardedLeaf value outside F)
      (movingGuardedExtra value outside (movingLocalExtra E)) n t small bulk XL XR =
      ∑ a : MovingSampleSlots σ n, (movingSamplesPrior μ a : ℂ) *
        movingSupportedWeight value outside (buildMovingSlotData n t small bulk a) XL XR
          (recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
            (movingSlotCutoff value childBound pivotBound (movingLocalExtra E)) n
            ⟨n, buildMovingSlotData n t small bulk a, XL, XR⟩ t) := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingSampledWeight, OAI.Ostmann.movingGuardedLeaf, OAI.Ostmann.movingGuardedExtra, OAI.Ostmann.movingLocalExtra, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.movingSupportedWeight, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff