MovingSupportWeight.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Separating the exact arithmetic indicator from the recursive weight

def OAI.Ostmann.movingUnrestrictedWeight line 12

Source documentation

Evaluation along the forced integer pivots with just the arithmetic indicators removed. The same leaf and node factors remain.

noncomputable def movingUnrestrictedWeight {σ : Type*} (value : σ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ)
    (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ) :
    {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → ℂ
  | _, .leaf s regular, XL, XR => F ⟨0, .leaf s regular, XL, XR⟩ s
  | n + 1, .node s CL CR u left right, XL, XR =>
      let p := (MovingSlotData.step s CL CR u left right false).naturalPivot value XL XR
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step

def OAI.Ostmann.movingArithmeticIndicator line 23
theorem OAI.Ostmann.movingSlotWeight_arithmeticSupport line 27

theorem OAI.Ostmann.MovingSlotData.ArithmeticSupport.integral line 45

Source documentation

The support indicator itself forces the exact positive integer recursion.

theorem MovingSlotData.ArithmeticSupport.integral {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ)
    (hsupport : T.ArithmeticSupport value childBound pivotBound XL XR) :
    T.Integral value XL XR := by
…

Mentions: OAI.Ostmann.MovingSlotData

theorem OAI.Ostmann.movingSlotWeight_eq_unrestricted line 81

Source documentation

On the derived support every guard evaluates to one, so only the original leaf weights and extra node factors remain.

theorem movingSlotWeight_eq_unrestricted {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (XL XR : ℕ) (hsupport : T.ArithmeticSupport value childBound pivotBound XL XR) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
      (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
        movingUnrestrictedWeight value F extra T XL XR := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingUnrestrictedWeight

theorem OAI.Ostmann.movingSlotWeight_indicator_factor line 122

Source documentation

This factorization includes every zero-support term; it is suitable for weighted prime sums without conditioning away the original arithmetic tests.

theorem movingSlotWeight_indicator_factor {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (hf : T.Frequencies (· ≠ 0)) (XL XR : ℕ) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
      (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
        movingArithmeticIndicator value childBound pivotBound T XL XR *
          movingUnrestrictedWeight value F extra T XL XR := by
…

theorem OAI.Ostmann.movingArithmeticIndicator_cells line 138