OAI/NumberTheory/TwoPoint/Bounds/DesignationWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.product_grouped_by_label line 13
2. lemma OAI.TwoPointCorrelations.mem_label_image_iff_count_pos line 19
3. lemma OAI.TwoPointCorrelations.label_image_product line 24
4. lemma OAI.TwoPointCorrelations.designated_weight_exponents line 45

   Source documentation

   The modulus atom appears once if there is any lit occurrence; unlit occurrences retain their individual scalar reciprocals.

   lemma designated_weight_exponents (L U : Finset τ) (label : τ → ι) (θ : ι → ℝ) :
       (∏ t ∈ U, θ (label t)) * (∏ i ∈ L.image label, θ i) =
         ∏ i, θ i ^ litReciprocalExponent
           (L.filter (fun t => label t = i)).card (U.filter (fun t => label t = i)).card := by
   …

   Mentions: OAI.TwoPointCorrelations.litReciprocalExponent

5. lemma OAI.TwoPointCorrelations.absolute_unlit_coefficient line 56
6. theorem OAI.TwoPointCorrelations.designated_reciprocal_extra_bound line 63

   Source documentation

   Exact baseline extraction for the designated reciprocal coefficient.

   theorem designated_reciprocal_extra_bound (L U : Finset τ) (label : τ → ι)
       (p : ι → ℝ) (H : ℝ)
       (hcount : ∀ i, 2 ≤ (L.filter (fun t => label t = i)).card +
         (U.filter (fun t => label t = i)).card)
       (hH : 0 < H) (hp : ∀ i, H ≤ p i) :
       (∏ t ∈ U, (p (label t))⁻¹) * (∏ i ∈ L.image label, (p i)⁻¹) ≤
         (∏ i, (p i)⁻¹) * H⁻¹ ^
           (∑ i, extraReciprocalExponent (L.filter (fun t => label t = i)).card
             (U.filter (fun t => label t = i)).card) := by
   …

   Mentions: OAI.TwoPointCorrelations.extraReciprocalExponent

7. theorem OAI.TwoPointCorrelations.designated_all_reciprocal_bound line 78

   Source documentation

   Including singleton atoms gives exactly one basic reciprocal for every observed label. Extra powers are still measured only by the nonsingleton lit and unlit counts; singleton labels have both counts zero.

   theorem designated_all_reciprocal_bound (S : Finset ι) (L U : Finset τ)
       (label : τ → ι) (p : ι → ℝ) (H : ℝ)
       (hzero : ∀ i ∈ S, (L.filter (fun t => label t = i)).card = 0 ∧
         (U.filter (fun t => label t = i)).card = 0)
       (hcount : ∀ i ∉ S, 2 ≤ (L.filter (fun t => label t = i)).card +
         (U.filter (fun t => label t = i)).card)
       (hH : 0 < H) (hp : ∀ i, H ≤ p i) :
       (∏ t ∈ U, (p (label t))⁻¹) * (∏ i ∈ L.image label, (p i)⁻¹) *
           (∏ i ∈ S, (p i)⁻¹) ≤
         (∏ i, (p i)⁻¹) * H⁻¹ ^
           (∑ i, extraReciprocalExponent (L.filter (fun t => label t = i)).card
             (U.filter (fun t => label t = i)).card) := by
   …

   Mentions: OAI.TwoPointCorrelations.extraReciprocalExponent