OAI/MeasureTheory/Falconer/Graphs/GraphScaleData.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The manuscript scales satisfy the analytic graph hypotheses

Depths a, p, v and L are normalized by the terminal depth. The actual radial frequency is supplied by 2^frequency = R^v. All dimensional constants and lower-scale requirements are explicit.

  1. def OAI.Falconer.graphDerivativeScale line 16
  2. theorem OAI.Falconer.graph_scale_data line 20
  3. theorem OAI.Falconer.eventually_graph_scale_constants line 90

    Source documentation

    The two fixed-dimensional lower-scale conditions hold at all sufficiently large terminal depths, with the derivative order already fixed.

    theorem eventually_graph_scale_constants (d : ℕ) {σ : ℝ} (hσ : 0 < σ) :
    ∀ᶠ N : ℕ in Filter.atTop,
      40*Real.sqrt d ≤ ((2 : ℝ)^N)^(20*σ) ∧
      4*Real.pi ≤ ((2 : ℝ)^N)^(20*σ) := by
…