FinitePriorComparison.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Joint approximation of the finite cell and residue distributions

The ideal coordinate masses may be as large as two because the exceptional real-character multiplier is retained. No independence approximation is assumed beyond the one-coordinate absolute errors.

theorem OAI.Ostmann.sum_cons line 18
theorem OAI.Ostmann.productPrior_mass_le_two_pow line 24
theorem OAI.Ostmann.productPrior_l1_comparison line 34

theorem OAI.Ostmann.weighted_productPrior_comparison line 82

Source documentation

The joint coordinate replacement for a bounded signed spectator and smooth amplitude. The exceptional-character factors remain in the priors.

theorem weighted_productPrior_comparison {A : Type*} [Fintype A] {n : ℕ}
    (μ ν : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hν : ∀ i a, 0 ≤ ν i a)
    (hmassμ : ∀ i, ∑ a, μ i a ≤ 2) (hmassν : ∀ i, ∑ a, ν i a ≤ 2)
    (δ B : ℝ) (hδ : 0 ≤ δ) (hB : 0 ≤ B)
    (hdist : ∀ i, ∑ a, |μ i a - ν i a| ≤ δ)
    (F : (Fin n → A) → ℂ) (hF : ∀ x, ‖F x‖ ≤ B) :
    ‖(∑ x, (productPrior μ x : ℂ) * F x) - (∑ x, (productPrior ν x : ℂ) * F x)‖ ≤
      B * n * δ * 2 ^ n := by
…

Mentions: OAI.Ostmann.productPrior

theorem OAI.Ostmann.weighted_productPrior_variation line 111

Source documentation

Freezing the smooth factor in each joint box only costs its uniform variation times the total mass.

theorem weighted_productPrior_variation {A : Type*} [Fintype A] {n : ℕ}
    (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, ∑ a, μ i a ≤ 2)
    (F G : (Fin n → A) → ℂ) (η : ℝ) (hη : 0 ≤ η) (hFG : ∀ x, ‖F x - G x‖ ≤ η) :
    ‖(∑ x, (productPrior μ x : ℂ) * F x) - (∑ x, (productPrior μ x : ℂ) * G x)‖ ≤
      η * 2 ^ n := by
…

Mentions: OAI.Ostmann.productPrior