BulkCellMixtures.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Reassembling log cells with the original normalization

def OAI.Ostmann.bulkCellMixture line 11
instance OAI.Ostmann.finite_bulkCellMixture line 14
theorem OAI.Ostmann.BulkIntegrand.average_cellMixture line 20

theorem OAI.Ostmann.BulkIntegrand.cellMixture_comparison line 33

Source documentation

Cell counts multiply only the approximation error. The original normalization is applied to both the prime and Page cell measures.

theorem BulkIntegrand.cellMixture_comparison {σ C : Type*} [Fintype σ] [Fintype C]
    (f : BulkIntegrand σ) (Z : ℝ) (hZ : 0 ≤ Z)
    (μ ν : C → Measure ℝ) [∀ c, IsFiniteMeasure (μ c)] [∀ c, IsFiniteMeasure (ν c)]
    (i : σ) (ε : C → ℝ)
    (hε : ∀ c x, ‖f.average (μ c) i x - f.average (ν c) i x‖ ≤ ε c) (x : σ → ℝ) :
    ‖f.average (bulkCellMixture Z μ) i x - f.average (bulkCellMixture Z ν) i x‖ ≤
      Z * ∑ c, ε c := by
…

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

theorem OAI.Ostmann.BulkIntegrand.cellMixtures_joint_comparison line 47

Source documentation

Joint cell reassembly uses bounded normalized masses, without inserting cell counts into the main term.

theorem BulkIntegrand.cellMixtures_joint_comparison {σ C : Type*} [Fintype σ] [Fintype C]
    (f : BulkIntegrand σ) (Z : σ → ℝ) (hZ : ∀ i, 0 ≤ Z i)
    (μ ν : σ → C → Measure ℝ)
    [∀ i c, IsFiniteMeasure (μ i c)] [∀ i c, IsFiniteMeasure (ν i c)]
    (order : List σ) (horder : order.Nodup)
    (hμ : ∀ i ∈ order, (bulkCellMixture (Z i) (μ i)).real Set.univ ≤ 2)
    (hν : ∀ i ∈ order, (bulkCellMixture (Z i) (ν i)).real Set.univ ≤ 2)
    (ε : σ → C → ℝ) (hε : ∀ i ∈ order, ∀ c, 0 ≤ ε i c)
    (herr : ∀ i ∈ order, ∀ c x,
      ‖f.average (μ i c) i x - f.average (ν i c) i x‖ ≤ ε i c) :
    ∀ x, ‖f.averages (fun i => bulkCellMixture (Z i) (μ i)) order x -
      f.averages (fun i => bulkCellMixture (Z i) (ν i)) order x‖ ≤
…

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