MovingSamplePairExpansion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact paired expansion of the fully supported sampled coefficient

The equality-pattern scalar is the literal original prior times all node compensations. The remaining coefficient retains every support test.

def OAI.Ostmann.movingCompensatedAverage line 14
theorem OAI.Ostmann.movingCompensatedAverage_pair line 18
theorem OAI.Ostmann.movingCompensatedAverage_pair_patterns line 35
Source documentation
The class assignments are injective, so coincidences are recorded exactly once; no independence is ascribed to their induced law.
```
theorem movingCompensatedAverage_pair_patterns {A : Type*} [Fintype A]
    (μ : ℕ → A → ℝ) (value : A → ℕ) (n : ℕ) (H K : MovingSampleSlots A n → ℂ) :
    letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
…
```
Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex
def OAI.Ostmann.movingSupportedSampleTerm line 56
def OAI.Ostmann.movingSupportedSampledWeight line 66
theorem OAI.Ostmann.movingSupportedSampledWeight_eq line 76

theorem OAI.Ostmann.movingSupportedSampledWeight_pair_patterns line 90

Source documentation

The original supported coefficient squared, in the coordinates used by Section 8's arithmetic comparison. Neither support nor the original weights are discarded in passing to equality patterns.

theorem movingSupportedSampledWeight_pair_patterns {σ : Type*} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (XL XR : ℕ) :
    letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex