PrimeRestorationDifference.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Deletion and collision errors for arbitrary signed prime observables

theorem OAI.Ostmann.finite_product_restoration_difference line 13

Source documentation

Monotone restoration costs exactly the excess mass of the product law. The observable can retain residue classes and every other arithmetic factor.

theorem finite_product_restoration_difference {J A : Type*} [Fintype J] [Fintype A]
    (μ ν : J → A → ℝ) (hμ : ∀ j a, 0 ≤ μ j a) (hle : ∀ j a, μ j a ≤ ν j a)
    (hmass : ∀ j, ∑ a, μ j a = 1) (F : (J → A) → ℂ)
    (B : ℝ) (hF : ∀ x, ‖F x‖ ≤ B) :
    ‖(∑ x, ((∏ j, μ j (x j) : ℝ) : ℂ) * F x) -
      ∑ x, ((∏ j, ν j (x j) : ℝ) : ℂ) * F x‖ ≤
      B * ((∏ j, ∑ a, ν j a) - 1) := by
…

theorem OAI.Ostmann.original_prime_restoration_difference line 37

Source documentation

Restoring deleted atoms retains the old normalization.

theorem original_prime_restoration_difference {J : Type*} [Fintype J]
    (P : Finset ℕ) (S D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hS : ∀ j, (∑ p ∈ S j \ D j, (p : ℝ)⁻¹) ≠ 0)
    (F : (J → P) → ℂ) (B : ℝ) (hF : ∀ x, ‖F x‖ ≤ B) :
    let Z := fun j => (∑ p ∈ S j \ D j, (p : ℝ)⁻¹)⁻¹
…

theorem OAI.Ostmann.norm_le_from_restoration line 76

theorem OAI.Ostmann.original_bulk_collision_restoration_bound line 87

Source documentation

The original injective expectation is bounded by the restored expectation, with separate collision and deleted-atom costs.

theorem original_bulk_collision_restoration_bound {J : Type*} [Fintype J]
    (P : Finset ℕ) (S D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hS : ∀ j, (∑ p ∈ S j \ D j, (p : ℝ)⁻¹) ≠ 0)
    (H T : ℝ) (hmass : ∀ j, (∑ p ∈ S j \ D j, (p : ℝ)⁻¹)⁻¹ ≤ Real.exp H)
    (hlow : ∀ j p, p ∈ S j \ D j → Real.exp T ≤ (p : ℝ))
    (F : (J → P) → ℂ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B)
    (M : ℝ)
    (hmain : ‖∑ x, ((∏ j, (if (x j : ℕ) ∈ S j then
      (∑ p ∈ S j \ D j, (p : ℝ)⁻¹)⁻¹ * (x j : ℝ)⁻¹ else 0) : ℝ) : ℂ) * F x‖ ≤ M) :
    ‖∑ x, ((∏ j, primeSubsetPrior P (S j \ D j) (x j) : ℝ) : ℂ) *
      (if Function.Injective x then F x else 0)‖ ≤
      M + B * (Fintype.card J : ℝ) ^ 2 * Real.exp (H - T) +
…

Mentions: OAI.Ostmann.primeSubsetPrior