VariableModulusSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Paired frequency bounds when each history pair has its own modulus

The common frequency modulus can depend on the two fixed histories. The upper bound is independent of its size; it comes from the reduced moduli at the individual nodes under the original independent unit law.

def OAI.Ostmann.variableModulusSupportSum line 16
theorem OAI.Ostmann.variableModulusSupportSum_le line 24

theorem OAI.Ostmann.variableModulusSupportSum_rate line 65

Source documentation

The sufficiently-large cutoff is uniform in the history-dependent moduli, including their full denominator powers.

theorem variableModulusSupportSum_rate (n : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∀ N V : ℕ, ∀ Δ : ℝ, ∀ S : Finset ℤ,
      (N : ℝ) ≤ Real.exp (C * m) →
      (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
      (∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) →
      ∀ Q : FrequencyTree (S × S) n → ℕ, ∀ [_hQ : ∀ t, NeZero (Q t)],
      ∀ data : (t : FrequencyTree (S × S) n) → (ZMod (Q t))ˣ →
        List (ZMod (Q t))ˣ → Option (ArithmeticSplitData (Q t) × ArithmeticSplitData (Q t)),
      (∀ t P past d e, data t P past = some (d, e) →
        d.hasFrequencies (treeNodeFrequencies S n t past.length).1 ∧
          e.hasFrequencies (treeNodeFrequencies S n t past.length).2) →
      Real.exp (-(2 ^ n : ℕ) * Δ + K) * variableModulusSupportSum S V n Q data ≤
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.treeNodeFrequencies, OAI.Ostmann.variableModulusSupportSum