The iteration lemma for decay estimates on concentric balls

Let φ be nonnegative and nondecreasing on (0, R], and suppose that

φ ρ ≤ A ((ρ / r)^α + ε) φ r + B r^β whenever 0 < ρ ≤ r ≤ R,

with A, B ≥ 0 and β < α. Fix γ < α. If ε ≤ ε₀, then

φ ρ ≤ C ((ρ / r)^γ φ r + B ρ^β) whenever 0 < ρ ≤ r ≤ R,

where ε₀ > 0 and C depend only on A, α, β and γ. Taking γ = β gives the usual form φ ρ ≤ C ((ρ / r)^β φ r + B ρ^β). So a small perturbation ε costs only an arbitrarily small part of the decay rate α of the unperturbed inequality, and the inhomogeneous term keeps its rate β.

This is the device that turns a comparison argument into a Morrey or Campanato estimate. In the Campanato approach to the Schauder estimates, φ ρ is an integral such as ∫_{B_ρ} ‖∇u‖² or ∫_{B_ρ} ‖∇u - (∇u)_ρ‖² for a solution u of an equation with variable coefficients. Comparing u on B_r with the solution of the equation with coefficients frozen at the centre gives the hypothesis: α is the decay exponent of the frozen problem, ε measures the oscillation of the coefficients on B_r, and B r^β comes from the data. With γ = β and r = R, the conclusion is a power bound φ ρ ≤ C' ρ^β, the kind of growth condition that Morrey's Dirichlet growth theorem and Campanato's characterization of Hölder continuity turn into Hölder estimates.

Main declarations

• TauCeti.exists_le_mul_div_rpow_mul_add_mul_rpow_of_le_mul_add: the iteration lemma.
• TauCeti.exists_le_mul_rpow_of_essOsc_step: the iteration lemma for an oscillation function with an additive inhomogeneity, turned into a bound φ s ≤ C (s / R)^β (Q + R^γ F).

References

• M. Giaquinta, Multiple Integrals in the Calculus of Variations and Nonlinear Elliptic Systems, Chapter III, Lemma 2.1.
• M. Giaquinta, L. Martinazzi, An Introduction to the Regularity Theory for Elliptic Systems, Harmonic Maps and Minimal Graphs, Lemma 5.13.
• Q. Han, F. Lin, Elliptic Partial Differential Equations, Lemma 3.4.

theorem TauCeti.exists_le_mul_div_rpow_mul_add_mul_rpow_of_le_mul_add {A α β γ : ℝ} (hA : 0 ≤ A) (hβ : β < α) (hγ : γ < α) : ∃ (ε₀ : ℝ) (C : ℝ), 0 < ε₀ ∧ 0 < C ∧ ∀ {φ : ℝ → ℝ} {R B ε : ℝ}, 0 ≤ B → ε ≤ ε₀ → MonotoneOn φ (Set.Ioc 0 R) → (∀ r ∈ Set.Ioc 0 R, 0 ≤ φ r) → (∀ (ρ r : ℝ), 0 < ρ → ρ ≤ r → r ≤ R → φ ρ ≤ A * ((ρ / r) ^ α + ε) * φ r + B * r ^ β) → ∀ (ρ r : ℝ), 0 < ρ → ρ ≤ r → r ≤ R → φ ρ ≤ C * ((ρ / r) ^ γ * φ r + B * ρ ^ β)

The iteration lemma. Let A ≥ 0 and β < α, and let γ < α. There are ε₀ > 0 and C > 0, depending only on A, α, β and γ, such that the following holds. Let φ be nonnegative and nondecreasing on (0, R], let B ≥ 0 and ε ≤ ε₀, and suppose that

φ ρ ≤ A ((ρ / r)^α + ε) φ r + B r^β whenever 0 < ρ ≤ r ≤ R.

Then

φ ρ ≤ C ((ρ / r)^γ φ r + B ρ^β) whenever 0 < ρ ≤ r ≤ R.

With γ = β this is the form φ ρ ≤ C ((ρ / r)^β φ r + B ρ^β) of the references.

theorem TauCeti.exists_le_mul_rpow_of_essOsc_step {α₀ C₀ K D γ : ℝ} (hα₀ : 0 < α₀) (hC₀ : 0 ≤ C₀) (hK : 0 ≤ K) (hD : 0 ≤ D) (hγ : 0 < γ) : ∃ (β : ℝ) (C : ℝ), 0 < β ∧ β < α₀ ∧ 0 < C ∧ ∀ {φ : ℝ → ℝ} {R s Q F : ℝ}, 0 < s → s ≤ R / 2 → 0 ≤ Q → 0 ≤ F → MonotoneOn φ (Set.Ioc 0 (R / 2)) → (∀ ρ ∈ Set.Ioc 0 (R / 2), 0 ≤ φ ρ) → φ (R / 2) ≤ 2 * (D * (Q + R ^ γ * F)) → (∀ (s ρ : ℝ), 0 < s → s ≤ ρ → ρ ≤ R / 2 → φ s ≤ C₀ * (s / ρ) ^ α₀ * φ ρ + K * ρ ^ γ * F) → φ s ≤ C * (s / R) ^ β * (Q + R ^ γ * F)

The iteration step of the interior oscillation estimate, as a statement about the essential oscillation φ alone. If φ s ≤ C₀ (s/ρ)^α₀ φ ρ + K ρ^γ F for s ≤ ρ ≤ R / 2, with φ nonnegative and monotone on (0, R/2] and φ (R / 2) ≤ 2 D (Q + R^γ F), then φ s ≤ C (s / R)^β (Q + R^γ F) for s ≤ R / 2, where β < α₀ and C > 0 depend only on α₀, C₀, K, D and γ.