OAI/NumberTheory/Ostmann/Construction/FixedInitialCutoffMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.initial_balanced_cell_mass_at line 11

   Source documentation

   The centers are fixed before the top and compensation priors are selected. Their balanced masses therefore remain available when the cells depend on them.

   theorem initial_balanced_cell_mass_at (P : Finset ℕ) (b d r m : ℕ)
       (μb : Fin b → P → ℝ) (μd : Fin d → P → ℝ) (μc : Fin r → P → ℝ)
       (gb : Fin b → P → Prop) (gd : Fin d → P → Prop) (gc : Fin r → P → Prop)
       (cb cd : ℝ)
       (hB : Real.exp (-(Real.log 2 + 2) * m) ≤
         ∑ x ∈ balancedTupleSet b gb, productPrior μb x *
           initialLogSumWeight (fun p : P => (p : ℕ)) cb x)
       (hD : Real.exp (-(Real.log 2 + 2) * m) ≤
         ∑ x ∈ balancedTupleSet d gd, productPrior μd x *
           initialLogSumWeight (fun p : P => (p : ℕ)) cd x)
       (hmc : ∀ i, ∑ p, μc i p = 1)
       (hgc : ∀ i p, μc i p ≠ 0 → gc i p) :
   …

   Mentions: OAI.Ostmann.balancedTupleSet, OAI.Ostmann.productPrior, OAI.Ostmann.initialLogSumWeight