OAI/NumberTheory/Ostmann/Construction/HistorySmoothFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The smooth factors in the expanded arithmetic histories

Compensation-prime powers and spectator transforms are excluded here, as in the definition of Xi in Section 8 of the manuscript.

  1. def OAI.Ostmann.archimedeanLeafFactor line 18
  2. theorem OAI.Ostmann.archimedeanLeafFactor_norm_le line 21
  3. inductive OAI.Ostmann.HistorySmoothData line 34
  4. def OAI.Ostmann.HistorySmoothData.value line 38
  5. def OAI.Ostmann.HistorySmoothData.Bounded line 44
  6. theorem OAI.Ostmann.HistorySmoothData.norm_value_le line 48
  7. theorem OAI.Ostmann.smooth_history_pair_norm_le line 67

    Source documentation

    There are two histories, each with exactly 2^n leaves. All node cutoffs have modulus at most one.

    theorem smooth_history_pair_norm_le {n : ℕ} (h₁ h₂ : HistorySmoothData n)
    (X B A : ℝ) (ψhat : ℝ → ℂ) (hB : 0 ≤ B) (hA : 0 ≤ A)
    (hψ : ∀ t, ‖ψhat t‖ ≤ B) (hh₁ : h₁.Bounded X B A) (hh₂ : h₂.Bounded X B A) :
    ‖h₁.value X ψhat * star (h₂.value X ψhat)‖ ≤ A ^ (2 * 2 ^ n) := by
…

    Mentions: OAI.Ostmann.HistorySmoothData