OAI/NumberTheory/Ostmann/Arithmetic/IntegerIntervalVariation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.complexIntegerInterval line 12
2. theorem OAI.Ostmann.complexIntegerInterval_add line 16
3. theorem OAI.Ostmann.integerLogCellMass_add line 23
4. theorem OAI.Ostmann.integerResidueAtom_nonneg line 29
5. theorem OAI.Ostmann.integerLogCellMass_nonneg line 34
6. theorem OAI.Ostmann.continuous_integerLogDensity line 38
7. theorem OAI.Ostmann.complexIntegerInterval_freeze line 41
8. theorem OAI.Ostmann.integerLogCellMass_partition line 66
9. theorem OAI.Ostmann.complexIntegerInterval_partition line 76
10. theorem OAI.Ostmann.weighted_integer_interval_variation line 88

    Source documentation

    The integer progression discrepancy pays total variation rather than the number of intervals. The normalization remains the original exp(-G).

    theorem weighted_integer_interval_variation (q a : ℕ) (hq : 0 < q) (G : ℝ)
        (s : ℕ → ℝ) (hs : Monotone s) (N : ℕ) (w : ℕ → ℂ) :
        ‖∑ j ∈ Finset.range N, w j *
          ((integerLogCellMass q a (s j) (s (j + 1)) G -
            ∫ y in Set.Ioc (s j) (s (j + 1)), integerLogDensity q G y : ℝ) : ℂ)‖ ≤
          discreteVariation w N * (2 * Real.exp (-G)) := by
    …

    Mentions: OAI.Ostmann.integerLogCellMass, OAI.Ostmann.integerLogDensity, OAI.Ostmann.discreteVariation