LitOccurrenceWeights.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact reciprocal exponent of each nonsingleton lit designation.

def OAI.TwoPointCorrelations.litReciprocalExponent line 11
def OAI.TwoPointCorrelations.extraReciprocalExponent line 14
lemma OAI.TwoPointCorrelations.litReciprocalExponent_pos line 17
lemma OAI.TwoPointCorrelations.unlit_le_twice_extra line 24
Source documentation
An entirely unlit nonsingleton uses at most half its exponent for the baseline reciprocal. Each unlit occurrence of a lit label is wholly extra.
```
lemma unlit_le_twice_extra (lit unlit : ℕ) (hm : 2 ≤ lit + unlit) :
    unlit ≤ 2 * extraReciprocalExponent lit unlit := by
…
```
Mentions: OAI.TwoPointCorrelations.extraReciprocalExponent
lemma OAI.TwoPointCorrelations.total_unlit_le_twice_extra line 29

lemma OAI.TwoPointCorrelations.lit_reciprocal_product_factor line 36

Source documentation

Factor off exactly one baseline reciprocal per nonsingleton label.

lemma lit_reciprocal_product_factor {ι : Type*} [Fintype ι]
    (lit unlit : ι → ℕ) (p : ι → ℝ) (hm : ∀ i, 2 ≤ lit i + unlit i) :
    (∏ i, (p i)⁻¹ ^ litReciprocalExponent (lit i) (unlit i)) =
      (∏ i, (p i)⁻¹) * ∏ i, (p i)⁻¹ ^ extraReciprocalExponent (lit i) (unlit i) := by
…

Mentions: OAI.TwoPointCorrelations.litReciprocalExponent, OAI.TwoPointCorrelations.extraReciprocalExponent

theorem OAI.TwoPointCorrelations.lit_reciprocal_product_bound line 52

Source documentation

Retain the baseline reciprocal weight and bound every extra power by H⁻¹; no nondivisibility condition is imposed on an unlit occurrence.

theorem lit_reciprocal_product_bound {ι : Type*} [Fintype ι]
    (lit unlit : ι → ℕ) (p : ι → ℝ) (H : ℝ)
    (hm : ∀ i, 2 ≤ lit i + unlit i) (hH : 0 < H) (hp : ∀ i, H ≤ p i) :
    (∏ i, (p i)⁻¹ ^ litReciprocalExponent (lit i) (unlit i)) ≤
      (∏ i, (p i)⁻¹) * H⁻¹ ^ (∑ i, extraReciprocalExponent (lit i) (unlit i)) := by
…

Mentions: OAI.TwoPointCorrelations.litReciprocalExponent, OAI.TwoPointCorrelations.extraReciprocalExponent