DivisorClasses.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.DivisorClasses.PrefixWitness line 13
Source documentation
The selected sorted prime-factor prefix, including both separation facts.
```
def PrefixWitness (n : ℕ) (Y : ℝ) (d p : ℕ) : Prop :=
…
```
def OAI.Problem337.DivisorClasses.LargeClass line 19
def OAI.Problem337.DivisorClasses.SmallClass line 23
def OAI.Problem337.DivisorClasses.BandClass line 27
theorem OAI.Problem337.DivisorClasses.class_cover line 34
Source documentation
Every integer belongs to one of the three actual prime-prefix regimes. No choice of prefix, divisor estimate, or distribution assertion is assumed.
```
theorem class_cover (n : ℕ) (S v Y : ℝ) (J : ℕ)
    (hY : 1 ≤ Real.sqrt Y)
    (hbands : ∀ w : ℝ, 4 * Real.log S ≤ w → w < v ^ (15 / 16 : ℝ) →
      ∃ j : ℕ, j < J ∧ DyadicBands.InBand (4 * Real.log S) j w) :
    LargeClass n v Y ∨ SmallClass n S v Y ∨
      ∃ j : ℕ, j < J ∧ BandClass n S v Y j := by
…
```
Mentions: OAI.Problem337.v, OAI.Problem337.DyadicBands.InBand, OAI.Problem337.DivisorClasses.LargeClass, OAI.Problem337.DivisorClasses.SmallClass, OAI.Problem337.DivisorClasses.BandClass
theorem OAI.Problem337.DivisorClasses.band_scale_lt line 53
Source documentation
An occupied intermediate class automatically has an admissible lower scale.
```
theorem band_scale_lt {n : ℕ} {S v Y : ℝ} {j : ℕ}
    (h : BandClass n S v Y j) :
    4 * Real.log S * 2 ^ j < v ^ (15 / 16 : ℝ) := by
…
```
Mentions: OAI.Problem337.v, OAI.Problem337.DivisorClasses.BandClass

theorem OAI.Problem337.DivisorClasses.sum_le_class_bounds line 61

Source documentation

Finite summation over the actual regimes. Overlap of prefix witnesses is harmless because all weights are nonnegative.

theorem sum_le_class_bounds {ι : Type*} (H : Finset ι) (n : ι → ℕ)
    (w : ι → ℝ) (S v Y : ℝ) (J : ℕ) (L M A : ℝ)
    (hY : 1 ≤ Real.sqrt Y)
    (hbands : ∀ x : ℝ, 4 * Real.log S ≤ x → x < v ^ (15 / 16 : ℝ) →
      ∃ j : ℕ, j < J ∧ DyadicBands.InBand (4 * Real.log S) j x)
    (hw : ∀ i ∈ H, 0 ≤ w i)
    (hlarge : (∑ i ∈ H with LargeClass (n i) v Y, w i) ≤ L)
    (hsmall : (∑ i ∈ H with SmallClass (n i) S v Y, w i) ≤ M)
    (hband : ∀ j < J, (∑ i ∈ H with BandClass (n i) S v Y j, w i) ≤ A) :
    (∑ i ∈ H, w i) ≤ L + M + (J : ℝ) * A := by
…

Mentions: OAI.Problem337.v, OAI.Problem337.DyadicBands.InBand, OAI.Problem337.DivisorClasses.LargeClass, OAI.Problem337.DivisorClasses.SmallClass, OAI.Problem337.DivisorClasses.BandClass