Statement file: Ingredients (Ingredients). This file contains exactly one declaration of the formalization's public statement surface.

structure AVenhance.Ingredients (β : ℝ) : Type

The exact list of ingredients of Section 2.1 (source lines 967-1396).

• one_lt_beta : 1 < β

  e.beta.def (977).

• beta_lt : β < 4 / 3

  e.beta.def (977).

• Λ : ℕ

  minimal scale separation, line 1030.

• two_pow_seven_le : 2 ^ 7 ≤ self.Λ

  Λ ∈ [2^7, ∞), line 1030.

• zeta : ℝ → ℝ

  time cutoff ζ, line 1226.

• zeta_smooth : ContDiff ℝ (↑⊤) self.zeta

  ζ ∈ C_c^∞(ℝ), line 1226.

• zeta_compact : HasCompactSupport self.zeta
• zeta_even (t : ℝ) : self.zeta (-t) = self.zeta t

  ζ even, line 1226.

• Czeta : ℝ

  the constant C_{e.zetatimecutoff}, lines 1226, 1235.

• one_le_Czeta : 1 ≤ self.Czeta
• zeta_nonneg (t : ℝ) : 0 ≤ self.zeta t

  0 ≤ ζ ≤ 1_{[-2/3,2/3]}, e.zetatimecutoff (1229).

• zeta_le_ind (t : ℝ) : self.zeta t ≤ indIcc (-(2 / 3)) (2 / 3) t
• zeta_partition (t : ℝ) : ∑' (k : ℤ), self.zeta (t - ↑k) = 1

  ∑_k ζ(· - k) ≡ 1, e.zetatimecutoff (1231).

• zeta_deriv_le (j : ℕ) : j ≤ Nstar β → ∀ (t : ℝ), |iteratedDeriv j self.zeta t| ≤ self.Czeta

  max_{j ≤ N_*} ‖∂_t^j ζ‖_∞ ≤ C, e.zetatimecutoff (1233-1235).

• zeta_sq_integral : ∫ (t : ℝ), self.zeta t ^ 2 = 9 / 10

  ∫ ζ² = 9/10, e.weirdo (1241).

• xi : ℝ → ℝ

  time cutoff ξ ∈ C^∞(ℝ), line 1268.

• xi_smooth : ContDiff ℝ (↑⊤) self.xi
• Cxi : ℝ

  the constant C_{e.cutoff.xi}, lines 1268, 1278.

• one_le_Cxi : 1 ≤ self.Cxi
• ind_le_xi (t : ℝ) : indIcc (-(3 / 4)) (3 / 4) t ≤ self.xi t

  1_{[-3/4,3/4]} ≤ ξ ≤ 1_{[-5/4,5/4]}, e.cutoff.xi (1271).

• xi_le_ind (t : ℝ) : self.xi t ≤ indIcc (-(5 / 4)) (5 / 4) t
• xi_partition (t : ℝ) : ∑' (k : { k : ℤ // Odd k }), self.xi (t - ↑↑k) = 1

  ∑_{k ∈ 2ℤ+1} ξ(· - k) ≡ 1, e.cutoff.xi (1273-1274).

• xi_deriv_le (j : ℕ) : j ≤ Nstar β → ∀ (t : ℝ), |iteratedDeriv j self.xi t| ≤ self.Cxi

  max_{j ≤ N_*} ‖∂_t^j ξ‖_∞ ≤ C, e.cutoff.xi (1276-1278).

• hatZeta : ℕ → ℝ → ℝ

  large-scale cutoffs ζ̂_{m,0}, ξ̂_{m,0}, m ∈ ℕ₀ (lines 1309-1322).

• hatXi : ℕ → ℝ → ℝ

  Enlarged auxiliary cutoff profile at each spatial scale.

• hatZeta_smooth (m : ℕ) : ContDiff ℝ (↑⊤) (self.hatZeta m)

  smoothness (implicit, see open questions).

• hatXi_smooth (m : ℕ) : ContDiff ℝ (↑⊤) (self.hatXi m)
• Chat : ℝ

  the constant C_{e.zeta.prime.ml.bounds} (line 1324).

• one_le_Chat : 1 ≤ self.Chat
• hatZeta_ge (m : ℕ) : 1 ≤ m → ∀ (l : ℤ) (t : ℝ), indIcc ((↑l - 1 / 2) * tauPP β self.Λ m + 2 * tauP β self.Λ m) ((↑l + 1 / 2) * tauPP β self.Λ m - 2 * tauP β self.Λ m) t ≤ shiftCutoff (self.hatZeta m) (↑l * tauPP β self.Λ m) t

  e.zeta.prime.ml.fitting (1327-1341), first line, lower bound.

• hatZeta_le (m : ℕ) : 1 ≤ m → ∀ (l : ℤ) (t : ℝ), shiftCutoff (self.hatZeta m) (↑l * tauPP β self.Λ m) t ≤ indIcc ((↑l - 1 / 2) * tauPP β self.Λ m + tauP β self.Λ m) ((↑l + 1 / 2) * tauPP β self.Λ m - tauP β self.Λ m) t

  e.zeta.prime.ml.fitting, first line, upper bound.

• hatXi_ge (m : ℕ) : 1 ≤ m → ∀ (l : ℤ) (t : ℝ), indIcc ((↑l - 1 / 2) * tauPP β self.Λ m + tauP β self.Λ m) ((↑l + 1 / 2) * tauPP β self.Λ m - tauP β self.Λ m) t ≤ shiftCutoff (self.hatXi m) (↑l * tauPP β self.Λ m) t

  e.zeta.prime.ml.fitting, second line, lower bound.

• hatXi_le (m : ℕ) : 1 ≤ m → ∀ (l : ℤ) (t : ℝ), shiftCutoff (self.hatXi m) (↑l * tauPP β self.Λ m) t ≤ indIcc ((↑l - 1 / 2) * tauPP β self.Λ m - tauP β self.Λ m) ((↑l + 1 / 2) * tauPP β self.Λ m + tauP β self.Λ m) t

  e.zeta.prime.ml.fitting, second line, upper bound.

• hatXi_partition (m : ℕ) : 1 ≤ m → ∀ (t : ℝ), ∑' (l : ℤ), shiftCutoff (self.hatXi m) (↑l * tauPP β self.Λ m) t = 1

  e.hatxi.partition (1346): ∑_l ξ̂_{m,l} = 1.

• hatZeta_deriv_le (m : ℕ) : 1 ≤ m → ∀ (l : ℤ), ∀ j ≤ Nstar β, ∀ (t : ℝ), tauP β self.Λ m ^ j * |iteratedDeriv j (shiftCutoff (self.hatZeta m) (↑l * tauPP β self.Λ m)) t| ≤ self.Chat

  e.zeta.prime.ml.bounds (1351-1359), for ζ̂.

• hatXi_deriv_le (m : ℕ) : 1 ≤ m → ∀ (l : ℤ), ∀ j ≤ Nstar β, ∀ (t : ℝ), tauP β self.Λ m ^ j * |iteratedDeriv j (shiftCutoff (self.hatXi m) (↑l * tauPP β self.Λ m)) t| ≤ self.Chat

  e.zeta.prime.ml.bounds, for ξ̂.