OAI/NumberTheory/Ostmann/Construction/MatchedHarmonicPrior.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.counterpartRoleFactor line 11
2. theorem OAI.Ostmann.counterpartRoleFactor_mem_Icc line 15
3. theorem OAI.Ostmann.matched_harmonic_prior line 23

   Source documentation

   Every counterpart role restriction is a unary factor on its matched actual prime. The normalizing constant and total prime product are exact.

   theorem matched_harmonic_prior {n : ℕ} (P : Finset ℕ)
       (Q : Fin n → Finset ℕ) (e : Equiv.Perm (Fin n)) (x : Fin n → P) :
       productPrior (fun i => primeSubsetPrior P (Q i)) (fun i => x (e i)) =
         (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * (∏ i, (x i : ℝ))⁻¹ *
           ∏ i, counterpartRoleFactor P Q e i (x i) := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.counterpartRoleFactor

4. theorem OAI.Ostmann.counterpartRoleFactor_norm line 41
5. theorem OAI.Ostmann.matched_harmonic_prior_normalized line 50

   Source documentation

   Extract the reciprocal scale before summing external pivots. On the stated product window the remaining ratio and all unary restrictions are bounded by one.

   theorem matched_harmonic_prior_normalized {n : ℕ} (P : Finset ℕ)
       (Q : Fin n → Finset ℕ) (e : Equiv.Perm (Fin n)) (x : Fin n → P)
       (X : ℝ) (hX : 0 < X) (hprod : X ≤ ∏ i, (x i : ℝ)) :
       ∃ U : ℝ, U ∈ Set.Icc 0 1 ∧
         productPrior (fun i => primeSubsetPrior P (Q i)) (fun i => x (e i)) =
           (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * X⁻¹ * U ∧
         U = (X / (∏ i, (x i : ℝ))) * ∏ i, counterpartRoleFactor P Q e i (x i) := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.counterpartRoleFactor