BulkWeightedCellComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Keep all cell and residue costs in the prime replacement error

theorem OAI.Ostmann.bulk_weighted_cell_comparison line 14

Source documentation

A residue-dependent arithmetic coefficient is held fixed during prime replacement. Its absolute value only multiplies the replacement error.

theorem bulk_weighted_cell_comparison {J C R : Type*}
    [Fintype J] [Fintype C] [Fintype R]
    (K : BulkIntegrand J) (a : R → ℂ) (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
    (μ ν : (J → C) → R → J → Measure ℝ)
    [∀ c z j, IsFiniteMeasure (μ c z j)] [∀ c z j, IsFiniteMeasure (ν c z j)]
    (E : (J → C) → R → ℝ)
    (hE : ∀ c z, ‖(∫ y, K y ∂Measure.pi (μ c z)) -
      ∫ y, K y ∂Measure.pi (ν c z)‖ ≤ E c z) :
    ‖((∏ j, Z j : ℝ) : ℂ) * ∑ c : J → C, ∑ z,
        ∫ y, (K.constMul (a z)) y ∂Measure.pi (μ c z) -
      ((∏ j, Z j : ℝ) : ℂ) * ∑ c : J → C, ∑ z,
        ∫ y, (K.constMul (a z)) y ∂Measure.pi (ν c z)‖ ≤
…

Mentions: OAI.Ostmann.BulkIntegrand

theorem OAI.Ostmann.bulk_weighted_cell_bound line 41

Source documentation

Combine the separately derived signed main term and replacement error.

theorem bulk_weighted_cell_bound {J C R : Type*}
    [Fintype J] [Fintype C] [Fintype R]
    (K : BulkIntegrand J) (a : R → ℂ) (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
    (μ ν : (J → C) → R → J → Measure ℝ)
    [∀ c z j, IsFiniteMeasure (μ c z j)] [∀ c z j, IsFiniteMeasure (ν c z j)]
    (E : (J → C) → R → ℝ)
    (hE : ∀ c z, ‖(∫ y, K y ∂Measure.pi (μ c z)) -
      ∫ y, K y ∂Measure.pi (ν c z)‖ ≤ E c z)
    (B : ℝ)
    (hmain : ‖((∏ j, Z j : ℝ) : ℂ) * ∑ c : J → C, ∑ z,
      ∫ y, (K.constMul (a z)) y ∂Measure.pi (ν c z)‖ ≤ B) :
    ‖((∏ j, Z j : ℝ) : ℂ) * ∑ c : J → C, ∑ z,
…

Mentions: OAI.Ostmann.BulkIntegrand