WordCellBulkGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact selected word cells in the bulk prime comparison

def OAI.Ostmann.wordCellSupport line 13
Source documentation
The selected integer log cell clipped to its original shell.
```
noncomputable def wordCellSupport (a b : ℝ) (h : ℕ) : Finset ℕ :=
…
```
theorem OAI.Ostmann.wordCellSupport_eq_filter line 16
theorem OAI.Ostmann.wordCellSupport_mass line 23
Source documentation
The cell mass used when selecting the word is precisely the mass used by its original normalized prime law in the subsequent comparison.
```
theorem wordCellSupport_mass (a b : ℝ) (D : Finset ℕ) (h : ℕ) :
    (∑ p ∈ wordCellSupport a b h \ D, (p : ℝ)⁻¹) =
      finiteCellMass (primeLogCellSet 1 0 a b \ D) primeLogIndex (fun p => (p : ℝ)⁻¹) h := by
…
```
Mentions: OAI.Ostmann.wordCellSupport, OAI.Ostmann.finiteCellMass, OAI.Ostmann.primeLogCellSet, OAI.Ostmann.primeLogIndex
theorem OAI.Ostmann.wordCellSupport_geometry line 29
theorem OAI.Ostmann.wordCellSupport_unit_residues line 44

theorem OAI.Ostmann.wordCellSupport_mass_lower line 55

Source documentation

The full cell has at least its mass after the fixed global exclusions.

theorem wordCellSupport_mass_lower (a b : ℝ) (D : Finset ℕ) (h : ℕ) (c : ℝ)
    (hm : c ≤ finiteCellMass (primeLogCellSet 1 0 a b \ D)
      primeLogIndex (fun p => (p : ℝ)⁻¹) h) :
    c ≤ ∑ p ∈ wordCellSupport a b h, (p : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.finiteCellMass, OAI.Ostmann.primeLogCellSet, OAI.Ostmann.primeLogIndex, OAI.Ostmann.wordCellSupport

theorem OAI.Ostmann.wordCellSupport_frozen_deletions line 65
Source documentation
Freezing nonbulk primes only enlarges the set deleted for the comparison; the law to which the answer is returned still has just its global exclusions.
```
theorem wordCellSupport_frozen_deletions {σ J : Type*} [Fintype σ]
    (a b : ℝ) (h : ℕ) (D : Finset ℕ) (base : σ → ℕ) (slot : J ↪ σ)
    (outside : List ℕ) :
    let deleted := D ∪ frozenPrimeDeletions base slot outside
…
```
Mentions: OAI.Ostmann.frozenPrimeDeletions