MovingFrequencyEnergy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Frequency energy under the unchanged internal sample law

theorem OAI.Ostmann.movingRootedFrequencyTree_injective line 11
theorem OAI.Ostmann.norm_sum_sq_single_support line 23

theorem OAI.Ostmann.movingRecursiveWeight_root_energy line 39

Source documentation

Fixing the original samples makes the descendant sum have at most one nonzero term. No bound by the number of frequency histories occurs.

theorem movingRecursiveWeight_root_energy {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound V : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (s : ℤ) (small bulk : TreeLeafTuple (List σ) n)
    (a : MovingSampleSlots σ n) (XL XR : ℕ) :
    let W := fun t => recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem

theorem OAI.Ostmann.scheduledFrequency_sum_rooted_real line 56

theorem OAI.Ostmann.movingSampledWeight_frequency_energy line 69

Source documentation

Jensen is applied only to the original independent sample law, after the unique-history square. All node compensations and guards remain in W.

theorem movingSampledWeight_frequency_energy {σ : Type*} [Fintype σ]
    (value : σ → ℕ) (μ : ℕ → σ → ℝ)
    (hμ : ∀ j a, 0 ≤ μ j a) (hmass : ∀ j, ∑ a, μ j a = 1)
    (childBound pivotBound V : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) :
    let W := fun t a => recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
…

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

theorem OAI.Ostmann.movingFrequencyCoefficient_energy line 116

Source documentation

The same estimate for the manuscript coefficient itself. The squared node-product is explicit, ready for the arithmetic support estimate; the spectators, Fourier factors and every support mask remain in the sample term.

theorem movingFrequencyCoefficient_energy {σ : Type} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (hμ : ∀ j a, 0 ≤ μ j a) (hmass : ∀ j, ∑ a, μ j a = 1)
    (childBound pivotBound V : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (small bulk : TreeLeafTuple (List σ) n) (XL XR : ℕ) :
    (∑ s : transferFrequencyRange (V n),
      ‖movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
        n s.val small bulk XL XR‖ ^ 2) ≤
      ∑ a : MovingSampleSlots σ n, movingSamplesPrior μ a *
        (movingSampleProduct value a : ℝ) ^ 2 *
        ∑ t : ScheduledFrequencyIndex V n,
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSamplesPrior, OAI.Ostmann.movingSampleProduct, OAI.Ostmann.ScheduledFrequencyIndex