Positive small-data thresholds

The scalar expression in the start estimate tends to zero with the data size. Its admissible threshold depends only on the numerical constants, before any solution or domain is chosen.

noncomputable def CKN.theoremAStartBound (q κ C₂₅ C₂₆ C₃₂ ε₀ : ℝ) : ℝ

The numerical upper bound for the initial theta quantity in lem:thmA-start.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.theoremAStartBound_continuous {q : ℝ} (hq : 0 < q) (κ C₂₅ C₂₆ C₃₂ : ℝ) : Continuous (theoremAStartBound q κ C₂₅ C₂₆ C₃₂)

The numerical start bound vanishes continuously with the data size.

theorem CKN.theoremAStartBound_zero {q : ℝ} (hq : 0 < q) (κ C₂₅ C₂₆ C₃₂ : ℝ) : theoremAStartBound q κ C₂₅ C₂₆ C₃₂ 0 = 0

At zero data the numerical start bound is zero.

theorem CKN.exists_theoremA_start_smallness (q C₂₅ C₂₆ C₂₇ C₂₈ C₃₂ : ℝ) (hq : 0 < q) (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ^ (1 / q) ≤ iterationLambda₀ C₂₇ C₂₈ ∧ theoremAStartBound q (iterationKappa C₂₇) C₂₅ C₂₆ C₃₂ ε₀ ≤ iterationEta C₂₇

A positive data threshold simultaneously satisfies the force and theta smallness requirements, with all constants fixed before the solution.