ExpandedScheduleWeight.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original atom weight is the concrete prime-word coefficient

def OAI.Ostmann.scheduleAtomTotal line 12
theorem OAI.Ostmann.expanded_schedule_leaf_total line 16
theorem OAI.Ostmann.recursiveTransferWeight_eq_zero_of_not_valid line 26

theorem OAI.Ostmann.expanded_schedule_weight_eq line 36

Source documentation

Expanding the constituents preserves the whole recursive weight, including invalid support, the forced pivots and all right conjugations.

theorem expanded_schedule_weight_eq {I α : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
    (F : ℕ → ℤ → ℂ) (depth n : ℕ) (hn : n ≤ depth) (path : List Bool)
    (current : CopyScheduleAtoms role n → List (ExpandedScheduledVariable α depth))
    (hc : ∀ i v, v ∈ current i → ExpandedCoordinateAfter n v)
    (x : ExpandedScheduledVariable α depth → ℕ) (t : FrequencyTree ℤ n) :
    recursiveTransferWeight (wordTransferSystem (ExpandedScheduledVariable α depth))
      (fun τ v => F (wordTransferLeafValue τ) v) (fun _ _ _ _ => 1) n
      ((expandedScheduledTemplate role (expandedPivotAddress α depth)
        childBound pivotBound n path current).state x) t =
    recursiveTransferWeight (scheduleAtomSystem role childBound pivotBound)
      (fun τ v => F (scheduleAtomTotal role τ) v) (fun _ _ _ _ => 1) n
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.ExpandedCoordinateAfter, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.wordTransferSystem, OAI.Ostmann.wordTransferLeafValue, OAI.Ostmann.expandedScheduledTemplate, OAI.Ostmann.expandedPivotAddress, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleAtomTotal

theorem OAI.Ostmann.expandedRootTemplate_weight_coefficient line 83

Source documentation

The original grouped-atom Fourier weight has an explicit polynomial coefficient on the independent constituent variables.

theorem expandedRootTemplate_weight_coefficient {I α : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (depth : ℕ) (words : CopyScheduleAtoms role depth → List α)
    (childBound pivotBound : ℕ → ℕ) (x : ExpandedScheduledVariable α depth → ℕ)
    (t : FrequencyTree ℤ depth) (ht : NonzeroInternalFrequencies depth t)
    (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y) (X lo hi : ℝ)
    (hlo : 1 ≤ lo) (hhi : lo ≤ hi) :
    recursiveTransferWeight (scheduleAtomSystem role childBound pivotBound)
      (fun τ v => (if (scheduleAtomTotal role τ : ℝ) / X ∈ Set.Icc lo hi then (1 : ℂ) else 0) *
        normalizedFourierProfile (𝓕 ψ : 𝓢(ℝ, ℂ)) v ((scheduleAtomTotal role τ : ℝ) / X))
      (fun _ _ _ _ => 1) depth
      ⟨depth, fun i => (((words i).map Sum.inl).map x).prod⟩ t =
      (WordFourierParameters.uniform depth (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).coefficient
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.scheduleAtomTotal, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.WordFourierParameters.uniform