Combining time-pairing moduli

The compactness lemma lem:compactness of the CKN manuscript asks for one modulus of the form A * |t - s| + B * |t - s| ^ θ for all indices of a sequence. In the blow-up limit (prop:blowup-limit) such moduli come with different exponents for finitely many indices and for a tail. On a bounded time interval these moduli combine into one of the same form.

theorem ESS.blowupLimitAssembly_rpow_le_max_mul_rpow {d L θ θ' : ℝ} (hd : 0 ≤ d) (hdL : d ≤ L) (hθ : 0 < θ) (hθθ' : θ ≤ θ') : d ^ θ' ≤ max 1 L ^ θ' * d ^ θ

On [0, L], a higher Hölder power is dominated by a lower one up to a constant factor.

theorem ESS.blowupLimitAssembly_modulus_or (g : ℕ → ℝ → ℝ) (a b : ℝ) (P Q : ℕ → Prop) (hP : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), P n → s ∈ Set.Icc a b → t ∈ Set.Icc a b → |g n t - g n s| ≤ A * dist t s + B * dist t s ^ θ) (hQ : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), Q n → s ∈ Set.Icc a b → t ∈ Set.Icc a b → |g n t - g n s| ≤ A * dist t s + B * dist t s ^ θ) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), P n ∨ Q n → s ∈ Set.Icc a b → t ∈ Set.Icc a b → |g n t - g n s| ≤ A * dist t s + B * dist t s ^ θ

Two moduli of the form A * d + B * d ^ θ, each valid on a subset of indices of a family of functions on a bounded interval, combine into one modulus of the same form valid on the union.

theorem ESS.blowupLimitAssembly_modulus_le (g : ℕ → ℝ → ℝ) (a b : ℝ) (hone : ∀ (n : ℕ), ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |g n t - g n s| ≤ A * dist t s + B * dist t s ^ θ) (j : ℕ) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), n ≤ j → s ∈ Set.Icc a b → t ∈ Set.Icc a b → |g n t - g n s| ≤ A * dist t s + B * dist t s ^ θ

Finitely many individual moduli of the form A * d + B * d ^ θ on a bounded interval combine into one.