MovingOuterVariationScale.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The moving-window budget for the original outer-prior kernel

theorem OAI.Ostmann.movingOuterVariationBudget_bound line 13

Source documentation

The two original outer factors and the diagonal reciprocal ratio cost only a fixed constant, uniformly in the giant cell centers.

theorem movingOuterVariationBudget_bound (ψ : 𝓢(ℝ, ℂ)) (V lo hi : ℝ)
    (n : ℕ) (B D : ℝ) (diagonal : Bool) :
    2 * giantOuterScalar diagonal * movingOuterVariationBudget ψ V lo hi n B D diagonal ≤
      (2 * Real.exp 1 * (2 * B + D * (Real.exp 2 - 1)) ^ 2 * (3 + Real.exp 2)) *
        (movingFourierVariationBudget ψ V lo hi n *
          (2 * B + D * (Real.exp 2 - 1)) ^ (2 ^ n - 1)) ^ 2 := by
…

Mentions: OAI.Ostmann.giantOuterScalar, OAI.Ostmann.movingOuterVariationBudget, OAI.Ostmann.movingFourierVariationBudget

theorem OAI.Ostmann.moving_outer_variation_scale line 33

Source documentation

Actual spectator growth, bounded harmonic normalizers and every moving bottom window fit the common giant comparison budget.

theorem moving_outer_variation_scale (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A Wwin B D H : ℝ) (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) (hH : 0 ≤ H) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L →
      let m := spectatorBulkCount k L
…

Mentions: OAI.Ostmann.spectatorBulkCount