OffWitnessEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed off-witness family has exponentially small coefficient norm

theorem OAI.Ostmann.eventual_off_witness_norm line 15

Source documentation

This is a conditional estimate for the explicitly defined subfamily where each small-kernel value is below the witness threshold. The pointwise condition is part of the subfamily, not an additional published input.

theorem eventual_off_witness_norm (C₀ ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ T : ℝ in atTop, ∀ (P : Finset ℕ) (M : ℕ) (S : Finset ℕ) (u : ℝ),
      (M : ℝ) ≤ Real.exp (C₀ * T) → (P.card : ℝ) ≤ T ^ (9999999 / 10000000 : ℝ) →
      (∀ s ∈ S, Squarefree s ∧ s ≤ M) → 0 ≤ u → u ≤ 4 * T ^ (1 / 1000000 : ℝ) →
      ∀ (c : Finset ℕ → ℂ) (G : Finset ℕ → ℕ → ℂ),
      (∀ U ∈ P.powerset, ‖c U‖ ≤ (1 / 16 : ℝ) ^ U.card) →
      (∀ s ∈ S, ∀ U ∈ P.powerset,
        ‖G U s‖ ≤ Real.exp (-9 * T ^ (9999999 / 10000000 : ℝ) / 10) * (Real.sqrt 2) ^ U.card) →
      Real.sqrt (∑ s ∈ S, (u ^ s.primeFactors.card / (s : ℝ)) *
        ‖∑ U ∈ P.powerset, c U * G U s‖ ^ 2) ≤
        Real.exp ((-4 / 5 + ε) * T ^ (9999999 / 10000000 : ℝ)) := by
…