FiniteCellPrior.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact pushforward to log-cell and residue coordinates

The finite partition of each actual prime sample induces independent cell priors. This is an equality, before any progression approximation is used.

def OAI.Ostmann.cellPrior line 15
theorem OAI.Ostmann.cellPrior_nonneg line 19
theorem OAI.Ostmann.cellPrior_mass line 28
theorem OAI.Ostmann.product_cell_indicator line 34
theorem OAI.Ostmann.product_cellPrior line 50

theorem OAI.Ostmann.sum_productPrior_cells line 62

Source documentation

Joint sampling and then recording cells is exactly sampling the cell priors. The statement keeps an arbitrary complex signed integrand.

theorem sum_productPrior_cells {A B : Type*} [Fintype A] [Fintype B] {n : ℕ}
    (μ : Fin n → A → ℝ) (cell : Fin n → A → B) (F : (Fin n → B) → ℂ) :
    (∑ x, (productPrior μ x : ℂ) * F (fun i => cell i (x i))) =
      ∑ y, (productPrior (fun i => cellPrior (μ i) (cell i)) y : ℂ) * F y := by
…

Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.cellPrior

theorem OAI.Ostmann.cellPrior_l1_le line 75

Source documentation

The per-class absolute error in the progression formula gives the one-coordinate total-variation estimate after summing the partition.

theorem cellPrior_l1_le {A B : Type*} [Fintype A] [Fintype B]
    (μ : A → ℝ) (cell : A → B) (ν : B → ℝ) (δ : ℝ)
    (h : ∀ b, |cellPrior μ cell b - ν b| ≤ δ) :
    (∑ b, |cellPrior μ cell b - ν b|) ≤ Fintype.card B * δ := by
…

Mentions: OAI.Ostmann.cellPrior

theorem OAI.Ostmann.cellPrior_mass_comparison line 85

Source documentation

The mass bound on the ideal prior follows from the actual mass and the cell errors, so it need not be an independent analytic hypothesis.

theorem cellPrior_mass_comparison {A B : Type*} [Fintype A] [Fintype B]
    (μ : A → ℝ) (cell : A → B) (ν : B → ℝ) (δ : ℝ)
    (h : ∀ b, |cellPrior μ cell b - ν b| ≤ δ) :
    (∑ b, ν b) ≤ (∑ a, μ a) + Fintype.card B * δ := by
…

Mentions: OAI.Ostmann.cellPrior

theorem OAI.Ostmann.finite_cell_idealization line 97

Source documentation

Joint finite-cell idealization, including the error from freezing the smooth amplitude. The residue correction is part of ν throughout.

theorem finite_cell_idealization {A C : Type*} [Fintype A] [Fintype C] {n : ℕ}
    (μ : Fin n → A → ℝ) (cell : Fin n → A → C) (ν : Fin n → C → ℝ)
    (hμ : ∀ i a, 0 ≤ μ i a) (hν : ∀ i c, 0 ≤ ν i c)
    (hmassμ : ∀ i, ∑ a, μ i a ≤ 2) (hmassν : ∀ i, ∑ c, ν i c ≤ 2)
    (δ B η : ℝ) (hδ : 0 ≤ δ) (hB : 0 ≤ B) (hη : 0 ≤ η)
    (hdist : ∀ i c, |cellPrior (μ i) (cell i) c - ν i c| ≤ δ)
    (H : (Fin n → A) → ℂ) (F : (Fin n → C) → ℂ)
    (hF : ∀ y, ‖F y‖ ≤ B) (hfreeze : ∀ x, ‖H x - F (fun i => cell i (x i))‖ ≤ η) :
    ‖(∑ x, (productPrior μ x : ℂ) * H x) -
      (∑ y, (productPrior ν y : ℂ) * F y)‖ ≤
        η * 2 ^ n + B * n * (Fintype.card C * δ) * 2 ^ n := by
…

Mentions: OAI.Ostmann.cellPrior, OAI.Ostmann.productPrior

theorem OAI.Ostmann.finite_cell_idealization_of_probability line 121

Source documentation

Joint idealization for probability samples. The ideal coordinate mass is at most two as a consequence of the per-cell approximation.

theorem finite_cell_idealization_of_probability {A C : Type*}
    [Fintype A] [Fintype C] {n : ℕ}
    (μ : Fin n → A → ℝ) (cell : Fin n → A → C) (ν : Fin n → C → ℝ)
    (hμ : ∀ i a, 0 ≤ μ i a) (hν : ∀ i c, 0 ≤ ν i c)
    (hmassμ : ∀ i, ∑ a, μ i a ≤ 1)
    (δ B η : ℝ) (hδ : 0 ≤ δ) (hB : 0 ≤ B) (hη : 0 ≤ η)
    (hsmall : Fintype.card C * δ ≤ 1)
    (hdist : ∀ i c, |cellPrior (μ i) (cell i) c - ν i c| ≤ δ)
    (H : (Fin n → A) → ℂ) (F : (Fin n → C) → ℂ)
    (hF : ∀ y, ‖F y‖ ≤ B) (hfreeze : ∀ x, ‖H x - F (fun i => cell i (x i))‖ ≤ η) :
    ‖(∑ x, (productPrior μ x : ℂ) * H x) -
      (∑ y, (productPrior ν y : ℂ) * F y)‖ ≤
…

Mentions: OAI.Ostmann.cellPrior, OAI.Ostmann.productPrior