MovingFrequencyCoefficient.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual sampled coefficient over its internal frequencies

def OAI.Ostmann.MovingDescendantFrequencyIndex line 13
Source documentation
The root frequency is fixed by the amplitude; only its descendants are summed here, each under its own level cutoff.
```
def MovingDescendantFrequencyIndex (V : ℕ → ℕ) : ℕ → Type
  | 0 => Unit
  | n + 1 => ScheduledFrequencyIndex V n × ScheduledFrequencyIndex V n
```
Mentions: OAI.Ostmann.ScheduledFrequencyIndex
instance OAI.Ostmann.movingDescendantFrequencyIndexFintype line 17
def OAI.Ostmann.movingRootedFrequencyTree line 21
def OAI.Ostmann.scheduledFrequencyRootEquiv line 26
theorem OAI.Ostmann.scheduledFrequencyRootEquiv_history line 32
theorem OAI.Ostmann.scheduledFrequency_sum_rooted line 40
Source documentation
The original root sum can be reindexed without counting a root twice.
```
theorem scheduledFrequency_sum_rooted (V : ℕ → ℕ) (n : ℕ)
    (f : FrequencyTree ℤ n → ℂ) :
    (∑ t : ScheduledFrequencyIndex V n, f (scheduledFrequencyHistory V n t)) =
      ∑ s : transferFrequencyRange (V n), ∑ t : MovingDescendantFrequencyIndex V n,
        f (movingRootedFrequencyTree V n s.val t) := by
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.scheduledFrequencyHistory, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.MovingDescendantFrequencyIndex, OAI.Ostmann.movingRootedFrequencyTree

def OAI.Ostmann.movingFrequencyCoefficient line 54

Source documentation

This is the current coefficient after the original internal prime samples and all descendant frequencies have been summed. Root guards remain in each term and are never turned into a conditioned probability law.

noncomputable def movingFrequencyCoefficient {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
    (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) : ℂ :=
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple

theorem OAI.Ostmann.movingFrequencyCoefficient_node line 66

Source documentation

At a successor level the two child histories are independent finite indices, while each root compensation vector is shared exactly once.

theorem movingFrequencyCoefficient_node {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
    (small bulk : TreeLeafTuple (List σ) (n + 1)) (XL XR : ℕ) :
    movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
      (n + 1) s small bulk XL XR =
      ∑ l : ScheduledFrequencyIndex V n, ∑ r : ScheduledFrequencyIndex V n,
        ∑ a : TreeLeafTuple (Fin 4 → σ) n,
          let u := movingCompensationSlots n a
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.movingCompensationSlots

theorem OAI.Ostmann.movingFrequencyCoefficient_original line 109

Source documentation

Identification with the already proved original prime-pattern expansion. This links the finite frequency coefficient to the arithmetic comparison.

theorem movingFrequencyCoefficient_original {σ I : Type} [Fintype σ]
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (μ : ℕ → σ → ℝ) (childBound pivotBound V : ℕ → ℕ)
    (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : SchwartzMap ℝ ℂ) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (s : ℤ) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) :
    movingFrequencyCoefficient value outside μ childBound pivotBound V
      (movingOriginalLeaf value q F g Dq S ψ X lo hi) φ G n s small bulk XL XR =
      ∑ t : MovingDescendantFrequencyIndex V n,
        movingOriginalSampleAverage q value outside μ childBound pivotBound F g Dq S ψ X lo hi φ G
          n (movingRootedFrequencyTree V n s t) small bulk XL XR := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.movingOriginalLeaf, OAI.Ostmann.MovingDescendantFrequencyIndex, OAI.Ostmann.movingOriginalSampleAverage, OAI.Ostmann.movingRootedFrequencyTree

theorem OAI.Ostmann.movingFrequencyCoefficient_square line 125

Source documentation

The frequency square has exactly two independent descendant histories. In particular no bound by the number of histories has been used here.

theorem movingFrequencyCoefficient_square {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
    (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) :
    ‖movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
      n s small bulk XL XR‖ ^ 2 =
      (∑ t : MovingDescendantFrequencyIndex V n, ∑ u : MovingDescendantFrequencyIndex V n,
        movingSupportedSampledWeight value outside μ childBound pivotBound F
          (movingOriginalNode value childBound pivotBound φ G) n
          (movingRootedFrequencyTree V n s t) small bulk XL XR *
        star (movingSupportedSampledWeight value outside μ childBound pivotBound F
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.MovingDescendantFrequencyIndex, OAI.Ostmann.movingSupportedSampledWeight, OAI.Ostmann.movingOriginalNode, OAI.Ostmann.movingRootedFrequencyTree