ContinuousIntegerComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous weights under the original external integer law

theorem OAI.Ostmann.complex_integer_density_freeze line 12

theorem OAI.Ostmann.integer_partition_variation line 44

Source documentation

A partition only incurs oscillation times total mass and interval length. Its progression error is bounded by variation independently of the mesh.

theorem integer_partition_variation (q a : ℕ) (hq : 0 < q) (G : ℝ)
    (s : ℕ → ℝ) (hs : Monotone s) (N : ℕ)
    (w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc (s 0) (s N))) (η : ℝ) (hη : 0 ≤ η)
    (hw : ∀ j < N, ∀ y ∈ Set.Ioc (s j) (s (j + 1)), ‖w y - w (s j)‖ ≤ η) :
    ‖complexIntegerInterval q a (s 0) (s N) G w -
        ∫ y in Set.Ioc (s 0) (s N), w y * (integerLogDensity q G y : ℂ)‖ ≤
      discreteVariation (fun j => w (s j)) N * (2 * Real.exp (-G)) +
      η * (integerLogCellMass q a (s 0) (s N) G + Real.exp (s N - G) * (s N - s 0)) := by
…

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

theorem OAI.Ostmann.continuous_integer_comparison line 105

Source documentation

The external integer comparison keeps the original normalization and requires no fixed mesh or partition-count loss.

theorem continuous_integer_comparison (q a : ℕ) (hq : 0 < q) (u v G : ℝ) (huv : u ≤ v)
    (w : ℝ → ℂ) (hwc : ContinuousOn w (Set.Icc u v)) (V : ℝ)
    (hV : ∀ (s : ℕ → ℝ), Monotone s → ∀ N, s 0 = u → s N = v →
      discreteVariation (fun j => w (s j)) N ≤ V) :
    ‖complexIntegerInterval q a u v G w -
        ∫ y in Set.Ioc u v, w y * (integerLogDensity q G y : ℂ)‖ ≤
      V * (2 * Real.exp (-G)) := by
…

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