SourcePredictableDecay.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial bounds for the source predictable-motion coefficient, before its dyadic gain is absorbed.

theorem OAI.LipschitzHilbert.source_blockCount_le_square line 12
theorem OAI.LipschitzHilbert.source_amplitude_log_factor line 28
theorem OAI.LipschitzHilbert.source_packet_polynomial line 49
theorem OAI.LipschitzHilbert.source_predictable_polynomial_bound line 77

theorem OAI.LipschitzHilbert.eventually_source_predictable_coefficient line 142

Source documentation

At the actual source step, the full predictable-motion coefficient is at most G^(-1/4), uniformly in the allowed phase and mass parameters.

theorem eventually_source_predictable_coefficient (p q D C Cfreq : ℝ)
    (hp : 0 ≤ p) (hq : 0 ≤ q) (hD : 0 ≤ D) (hC : 1 ≤ C) (hCfreq : 0 ≤ Cfreq) :
    ∀ᶠ L : ℝ in Filter.atTop,
      ∀ (A maskExponent Kw S a Z : ℝ) (K : ℕ),
      0 ≤ A → A ≤ L^q → 0 ≤ maskExponent → 1 ≤ Kw →
      0 ≤ a → a ≤ 1 → 0 ≤ Z → Z ≤ 2*L^2 → (K:ℝ) ≤ L^2 →
      Real.log (max 1 S) ≤ 3*L →
      let G := SourceParameters.step L
…

Mentions: OAI.LipschitzHilbert.SourceParameters.step