SourceCountParameters.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual dyadic source parameters meet the counting hypotheses.

theorem OAI.LipschitzHilbert.SourceParameters.blockCount_pos line 15
theorem OAI.LipschitzHilbert.SourceParameters.one_lt_step line 19
theorem OAI.LipschitzHilbert.SourceParameters.one_lt_branching line 23
theorem OAI.LipschitzHilbert.SourceParameters.log_branching_lower line 26
theorem OAI.LipschitzHilbert.SourceParameters.eventually_branching_ge line 36

theorem OAI.LipschitzHilbert.SourceParameters.eventually_count_parameters line 48

Source documentation

For every fixed enlargement and polynomial, the actual integer bin count and the manuscript's width/cutoff scales satisfy all numerical conditions used in the simultaneous count.

theorem eventually_count_parameters (p c C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop,
      1 < branching L ∧ 0 < (branchingNat L) ^ 2 ∧
      c ≤ ((branchingNat L) ^ 2 : ℕ) ∧
      (((branchingNat L) ^ 2 : ℕ) : ℝ) = branching L ^ 2 ∧
      ∀ m tau : ℝ,
        Real.exp (L ^ (9 / 10 : ℝ)) ≤ m →
        m ≤ 2 * Real.exp (L ^ (9 / 10 : ℝ)) →
        0 ≤ tau → tau ≤ Real.exp (-(L ^ (97 / 100 : ℝ))) →
        branching L ^ 2 ≤ m ∧
        ∀ ell : ℝ, 0 ≤ ell → ell ≤ tau → C * L ^ p * m * ell ≤ 1 / 2 := by
…

Mentions: OAI.LipschitzHilbert.SourceParameters.branching, OAI.LipschitzHilbert.SourceParameters.branchingNat