OAI/NumberTheory/Ostmann/Arithmetic/BulkDeletionCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_deleted_reciprocal_mass_le line 11
2. theorem OAI.Ostmann.bulk_deleted_product_cost line 27

   Source documentation

   All deleted values are charged using the old normalizers. If their total mass is at most one, the product excess is at most twice that mass.

   theorem bulk_deleted_product_cost {J : Type*} [Fintype J]
       (S D : J → Finset ℕ) (Z : J → ℝ) (H T K : ℝ)
       (hZ0 : ∀ j, 0 ≤ Z j) (hZ : ∀ j, Z j ≤ Real.exp H)
       (hcard : ∀ j, (D j).card ≤ K)
       (hlow : ∀ j q, q ∈ S j → Real.exp T ≤ (q : ℝ))
       (hsmall : (Fintype.card J : ℝ) * K * Real.exp (H - T) ≤ 1) :
       (∏ j, (1 + Z j * ∑ q ∈ S j ∩ D j, (q : ℝ)⁻¹)) - 1 ≤
         2 * (Fintype.card J : ℝ) * K * Real.exp (H - T) := by
   …