OAI/NumberTheory/JointDickman/Amplification/WeightedEndpointPair.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.weighted_endpoint_change_of_measure line 10
2. theorem OAI.JointDickman.weighted_endpoint_pair_change_of_measure line 29

   Source documentation

   Exact factorization of the first-representation measure at both endpoints. The test may depend jointly on both reconstructed site types.

   theorem weighted_endpoint_pair_change_of_measure {B : ℕ} {A D : Finset ℕ}
       (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
       (F : Finset ℕ → Finset ℕ → ℝ) :
       (∑ S ∈ (auxiliaryPrimes B).powerset, ∑ R ∈ (auxiliaryPrimes B).powerset,
         if A ⊆ S ∧ D ⊆ R then
           bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) S*
           bernoulliSubsetMass (auxiliaryPrimes B) (fun p => 1/(p : ℝ)) R*
           residueBaseWeight B (S \ A)*residueBaseWeight B (R \ D)*F S R else 0) =
         (remainderTiltNormalizer B A/(∏ p ∈ A, p : ℕ))*
         (remainderTiltNormalizer B D/(∏ p ∈ D, p : ℕ))*
           ∑ U ∈ (auxiliaryPrimes B \ A).powerset,
             ∑ V ∈ (auxiliaryPrimes B \ D).powerset,
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.bernoulliSubsetMass, OAI.JointDickman.residueBaseWeight, OAI.JointDickman.remainderTiltNormalizer