InternalPatternWeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Retaining the line-probability scale in an internal-prime pattern

def OAI.Ostmann.internalPatternWeight line 13
Source documentation
The coefficient before the simultaneous line probabilities includes one factor of the prime for every original compensation occurrence.
```
noncomputable def internalPatternWeight {I C A : Type*} [Fintype I]
    (pattern : I → C) (μ : I → A → ℝ) (prime : A → ℕ) (x : C → A) : ℝ :=
…
```

theorem OAI.Ostmann.internalPatternWeight_bound line 20

Source documentation

Collapsing equal samples keeps the prior at one fixed representative and charges only the repeated occurrences. The estimate also covers the larger 1/(p-1) line probability and hence the actual mixed 1/p law.

theorem internalPatternWeight_bound {I C A : Type*} [Fintype I] [Fintype C]
    (pattern : I → C) (rep : ∀ c, {i : I // pattern i = c})
    (μ : I → A → ℝ) (prime : A → ℕ) (E : ℝ)
    (hprime : ∀ a, (prime a).Prime)
    (hμ : ∀ i a, 0 ≤ μ i a) (hbound : ∀ i a, (prime a : ℝ) * μ i a ≤ E)
    (x : C → A) :
    internalPatternWeight pattern μ prime x * (∏ c, (prime (x c) : ℝ)⁻¹) ≤
      ((2 : ℝ) ^ Fintype.card C * E ^ (Fintype.card I - Fintype.card C)) *
        ∏ c, μ (rep c).val (x c) := by
…

Mentions: OAI.Ostmann.internalPatternWeight

theorem OAI.Ostmann.internalPatternWeight_complex_bound line 39