GoodCellSelection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Selecting many heavy cells with positive mean

def OAI.Ostmann.positiveHeavyCells line 12

theorem OAI.Ostmann.positiveHeavyCells_mass line 17

Source documentation

Removing low-mass cells from a positively biased shell retains a fixed amount of mass.

theorem positiveHeavyCells_mass (I : Finset ℕ) (w score : ℕ → ℝ) (δ θ : ℝ)
    (hw : ∀ h ∈ I, 0 ≤ w h) (hδ : 0 ≤ δ) (hθ : 0 ≤ θ)
    (hscore : ∀ h ∈ I, score h ≤ 1)
    (hbias : δ * (∑ h ∈ I, w h) ≤ ∑ h ∈ I, w h * score h)
    (hthin : I.card * θ ≤ (δ / 4) * ∑ h ∈ I, w h) :
    (δ / 4) * (∑ h ∈ I, w h) ≤ ∑ h ∈ positiveHeavyCells I w score δ θ, w h := by
…

Mentions: OAI.Ostmann.positiveHeavyCells

theorem OAI.Ostmann.positiveHeavyCells_card line 47

Source documentation

A cellwise upper mass bound converts retained mass into a lower bound on the number of usable cell indices.

theorem positiveHeavyCells_card (I : Finset ℕ) (w score : ℕ → ℝ) (δ θ M : ℝ)
    (hw : ∀ h ∈ I, 0 ≤ w h) (hδ : 0 ≤ δ) (hθ : 0 ≤ θ)
    (hscore : ∀ h ∈ I, score h ≤ 1)
    (hbias : δ * (∑ h ∈ I, w h) ≤ ∑ h ∈ I, w h * score h)
    (hthin : I.card * θ ≤ (δ / 4) * ∑ h ∈ I, w h)
    (hcap : ∀ h ∈ I, w h ≤ M) :
    (δ / 4) * (∑ h ∈ I, w h) ≤
      (positiveHeavyCells I w score δ θ).card * M := by
…

Mentions: OAI.Ostmann.positiveHeavyCells

theorem OAI.Ostmann.dense_index_target line 65

Source documentation

An arbitrary dense set of cell indices has the required target words; its minimum and maximum need not be chosen in advance.

theorem dense_index_target (δ : ℝ) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (I : Finset ℕ) (B : ℕ),
      (∀ x ∈ I, x ≤ B) → δ * B + 2 ≤ I.card → ∀ T : ℝ,
      C * B ≤ T → ∃ (n : ℕ) (w : List ℕ),
      w.length = n ∧ (∀ x ∈ w, x ∈ I) ∧ |(w.sum : ℝ) - T| < δ⁻¹ ∧
      (n : ℝ) * B ≤ 2 * T / δ ∧ T < (n + 1 : ℕ) * B := by
…