InitialLogSumBins.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic cutoff weights in the initial half-list

theorem OAI.Ostmann.logCellProfile_sum_centers line 14
Source documentation
Every nonzero translate on this bounded range is retained, including both boundary centers.
```
theorem logCellProfile_sum_centers (N : ℕ) (x : ℝ) (hx : 0 ≤ x) (hN : x ≤ N) :
    (∑ c ∈ Finset.Icc (0 : ℤ) N, logCellProfile (x - c)) = 1 := by
…
```
Mentions: OAI.Ostmann.logCellProfile

theorem OAI.Ostmann.exists_weighted_log_sum_center line 31

Source documentation

Pigeonholing selects a weight, without changing the underlying law.

theorem exists_weighted_log_sum_center {A : Type*} [Fintype A]
    (weight score : A → ℝ) (N : ℕ) (β : ℝ)
    (hmass : β ≤ ∑ a, weight a)
    (hscore : ∀ a, 0 ≤ score a ∧ score a ≤ N) :
    ∃ c ∈ Finset.Icc (0 : ℤ) N,
      β / (N + 1) ≤ ∑ a, weight a * logCellProfile (score a - c) := by
…

Mentions: OAI.Ostmann.logCellProfile

def OAI.Ostmann.balancedTupleSet line 51
theorem OAI.Ostmann.balancedTupleSet_mass line 55

theorem OAI.Ostmann.exists_balanced_log_sum_center line 79

Source documentation

The lower bound used for each broad-band group in Section 7.2.

theorem exists_balanced_log_sum_center {A : Type*} [Fintype A] (n : ℕ)
    (μ : Fin n → A → ℝ) (good : Fin n → A → Prop) (score : (Fin n → A) → ℝ)
    (N : ℕ) (δ : ℝ) (hδ : 0 ≤ δ)
    (hmass : ∀ i, δ ≤ ∑ a, if good i a then μ i a else 0)
    (hscore : ∀ x, 0 ≤ score x ∧ score x ≤ N) :
    ∃ c ∈ Finset.Icc (0 : ℤ) N,
      δ ^ n / (N + 1) ≤ ∑ x ∈ balancedTupleSet n good,
        productPrior μ x * logCellProfile (score x - c) := by
…

Mentions: OAI.Ostmann.balancedTupleSet, OAI.Ostmann.productPrior, OAI.Ostmann.logCellProfile