OAI/NumberTheory/Ostmann/Arithmetic/BulkBoxReassembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_box_sum_bound line 13

   Source documentation

   Reassembling boxes costs the product of their normalized masses. It does not cost the number of boxes in the main term.

   theorem bulk_box_sum_bound {J C : Type*} [Fintype J] [Fintype C]
       (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j) (H : J → C → ℝ)
       (hH : ∀ j c, 0 ≤ H j c) (hmass : ∀ j, Z j * ∑ c, H j c ≤ 2)
       (B : ℝ) (hB : 0 ≤ B) (E : (J → C) → ℂ)
       (hE : ∀ c, ‖E c‖ ≤ B * ∏ j, H j (c j)) :
       ‖((∏ j, Z j : ℝ) : ℂ) * ∑ c, E c‖ ≤ B * 2 ^ Fintype.card J := by
   …

2. theorem OAI.Ostmann.BulkIntegrand.integral_product_mixtures_bound line 37

   Source documentation

   The same bound for the exact normalized product of cell measures.

   theorem BulkIntegrand.integral_product_mixtures_bound {J C : Type*} [Fintype J] [Fintype C]
       (f : BulkIntegrand J) (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
       (μ : J → C → Measure ℝ) [∀ j c, IsFiniteMeasure (μ j c)]
       (H : J → C → ℝ) (hH : ∀ j c, 0 ≤ H j c)
       (hmass : ∀ j, Z j * ∑ c, H j c ≤ 2)
       (B : ℝ) (hB : 0 ≤ B)
       (hbox : ∀ c : J → C,
         ‖∫ x, f x ∂Measure.pi (fun j => μ j (c j))‖ ≤ B * ∏ j, H j (c j)) :
       ‖∫ x, f x ∂Measure.pi (fun j => bulkCellMixture (Z j) (μ j))‖ ≤ B * 2 ^ Fintype.card J := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.bulkCellMixture