OAI/NumberTheory/Ostmann/Construction/InitialHalfListWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.initialLogSumWeight line 11
2. theorem OAI.Ostmann.initialLogSumWeight_nonneg line 15
3. theorem OAI.Ostmann.initialLogSumWeight_le_one line 19
4. theorem OAI.Ostmann.balancedHalfMass_append line 25

   Source documentation

   Joining the bulk and spectator groups preserves the two weights and both balanced events under their original independent priors.

   theorem balancedHalfMass_append {A : Type*} [Fintype A] (b d : ℕ)
       (μ : Fin b → A → ℝ) (ν : Fin d → A → ℝ)
       (goodB : Fin b → A → Prop) (goodD : Fin d → A → Prop)
       (wB : (Fin b → A) → ℝ) (wD : (Fin d → A) → ℝ) :
       (∑ x ∈ balancedTupleSet (b + d) (Fin.append goodB goodD),
         productPrior (Fin.append μ ν) x *
           (wB (fun i => x (i.castAdd d)) * wD (fun i => x (i.natAdd b)))) =
         (∑ x ∈ balancedTupleSet b goodB, productPrior μ x * wB x) *
           ∑ x ∈ balancedTupleSet d goodD, productPrior ν x * wD x := by
   …

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

5. theorem OAI.Ostmann.balancedHalfMass_log_weights_lower line 52

   Source documentation

   The two selected cutoffs together retain a fixed exponential amount of balanced mass. Their product is still a weight, not a conditioned law.

   theorem balancedHalfMass_log_weights_lower {A : Type*} [Fintype A] (b d m : ℕ)
       (value : A → ℕ) (μ : Fin b → A → ℝ) (ν : Fin d → A → ℝ)
       (goodB : Fin b → A → Prop) (goodD : Fin d → A → Prop)
       (cb cd C : ℝ)
       (hB : Real.exp (-C * m) ≤
         ∑ x ∈ balancedTupleSet b goodB, productPrior μ x * initialLogSumWeight value cb x)
       (hD : Real.exp (-C * m) ≤
         ∑ x ∈ balancedTupleSet d goodD, productPrior ν x * initialLogSumWeight value cd x) :
       Real.exp (-(2 * C) * m) ≤
         ∑ x ∈ balancedTupleSet (b + d) (Fin.append goodB goodD),
           productPrior (Fin.append μ ν) x *
             (initialLogSumWeight value cb (fun i => x (i.castAdd d)) *
   …

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