OAI/NumberTheory/Ostmann/Construction/FinitePairCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_cellPrior_mul line 11
2. theorem OAI.Ostmann.sum_pair_cells line 21
3. theorem OAI.Ostmann.pair_prior_l1 line 36
4. theorem OAI.Ostmann.weighted_sum_difference line 62
5. theorem OAI.Ostmann.finite_pair_cell_idealization line 79

   Source documentation

   The two giant spaces can be different. The original priors have mass at most one; the ideal mass bound is derived from their cell errors.

   theorem finite_pair_cell_idealization {A B C D : Type*}
       [Fintype A] [Fintype B] [Fintype C] [Fintype D]
       (μ : A → ℝ) (ρ : B → ℝ) (c : A → C) (d : B → D)
       (ν : C → ℝ) (σ : D → ℝ)
       (hμ : ∀ a, 0 ≤ μ a) (hρ : ∀ b, 0 ≤ ρ b) (hν : ∀ a, 0 ≤ ν a)
       (hmassμ : ∑ a, μ a ≤ 1) (hmassρ : ∑ b, ρ b ≤ 1)
       (δ ε K η : ℝ) (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hK : 0 ≤ K) (hη : 0 ≤ η)
       (hsmall : Fintype.card C * δ ≤ 1)
       (hdistμ : ∀ a, |cellPrior μ c a - ν a| ≤ δ)
       (hdistρ : ∀ b, |cellPrior ρ d b - σ b| ≤ ε)
       (H : A × B → ℂ) (F : C × D → ℂ)
       (hF : ∀ y, ‖F y‖ ≤ K) (hfreeze : ∀ x, ‖H x - F (c x.1, d x.2)‖ ≤ η) :
   …

   Mentions: OAI.Ostmann.cellPrior