PatternFrequencyNormSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the arithmetic norm over frequencies and internal patterns

theorem OAI.Ostmann.paired_frequency_norm_sum_le line 13

Source documentation

The two-history norm retains every node's reduced-modulus bound. Only the negligible comparison errors are multiplied by the full history count.

theorem paired_frequency_norm_sum_le (S : Finset ℤ) (n N V : ℕ)
    (D K err : ℝ) (hD : 0 ≤ D) (hK : 0 ≤ K)
    (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
    (hdiv : ∀ q : ℕ, q ≠ 0 → q ≤ N ^ 2 → (q.divisors.card : ℝ) ≤ D)
    (R : FrequencyTree (S × S) n → ℂ)
    (hR : ∀ t, ‖R t‖ ≤ err + K *
      (frequencyLeafWeight (pairedFrequencyLeaf S V) n t *
        ((frequencySplitList S n t).map (pairFrequencySupportBound D)).prod)) :
    ‖∑ t, R t‖ ≤ (Fintype.card (FrequencyTree (S × S) n) : ℝ) * err +
      K * ((8 * D ^ 4 * (1 + Real.log N) ^ 3) ^ (2 ^ n - 1) *
        (2 * (V : ℝ)) ^ (2 * 2 ^ n)) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.pairedFrequencyLeaf, OAI.Ostmann.frequencySplitList, OAI.Ostmann.pairFrequencySupportBound

theorem OAI.Ostmann.pattern_frequency_norm_sum_le line 40

Source documentation

The same retained frequency sum survives summing every equality pattern of the original internal prime samples.

theorem pattern_frequency_norm_sum_le (S : Finset ℤ) (n N V : ℕ)
    (D E K err : ℝ) (hD : 0 ≤ D) (hE : 0 ≤ E) (hK : 0 ≤ K) (herr : 0 ≤ err)
    (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
    (hdiv : ∀ q : ℕ, q ≠ 0 → q ≤ N ^ 2 → (q.divisors.card : ℝ) ≤ D) :
    let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

Mentions: OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex