Picard iteration for a quadratic map in the intersection of two Lebesgue spaces #
The fixed point of prop:pv-local-solution is obtained by iterating the Duhamel
map from the heat orbit. We record the iteration abstractly: a map on functions
which is quadratically Lipschitz for the norm ‖·‖_p + ‖·‖_q has a fixed point
(up to null sets) as soon as its value at the origin is small.
theorem
ESS.picard_limit_of_geometric
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
{p : ENNReal}
(hp : 1 ≤ p)
{f : ℕ → α → E}
(hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ)
{d : ENNReal}
(hd : d ≠ ⊤)
(hstep : ∀ (n : ℕ), 2 ^ n * MeasureTheory.eLpNorm (f (n + 1) - f n) p μ ≤ d)
:
∃ (g : α → E),
MeasureTheory.MemLp g p μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
A sequence of functions whose consecutive L^p distances decay
geometrically has an L^p limit.
theorem
ESS.picard_limits_ae_eq
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
{p q : ENNReal}
(hp : p ≠ 0)
(hq : q ≠ 0)
{f : ℕ → α → E}
{g g' : α → E}
(hg : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0))
(hg' : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g') q μ) Filter.atTop (nhds 0))
:
g =ᵐ[μ] g'
Limits in two Lebesgue norms of the same sequence agree almost everywhere.
theorem
ESS.picard_fixedPoint
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[CompleteSpace E]
{p q : ENNReal}
(hp : 1 ≤ p)
(hq : 1 ≤ q)
(Φ : (α → E) → α → E)
(h : α → E)
{K : ENNReal}
(hK : K ≠ ⊤)
(hhp : MeasureTheory.MemLp h p μ)
(hhq : MeasureTheory.MemLp h q μ)
(hmaps :
∀ (U : α → E),
MeasureTheory.MemLp U p μ →
MeasureTheory.MemLp U q μ → MeasureTheory.MemLp (Φ U) p μ ∧ MeasureTheory.MemLp (Φ U) q μ)
(hlip :
∀ (U V : α → E),
MeasureTheory.MemLp U p μ →
MeasureTheory.MemLp U q μ →
MeasureTheory.MemLp V p μ →
MeasureTheory.MemLp V q μ →
MeasureTheory.eLpNorm (Φ U - Φ V) p μ + MeasureTheory.eLpNorm (Φ U - Φ V) q μ ≤ K * (MeasureTheory.eLpNorm (U - V) p μ + MeasureTheory.eLpNorm (U - V) q μ) * (MeasureTheory.eLpNorm U p μ + MeasureTheory.eLpNorm U q μ + (MeasureTheory.eLpNorm V p μ + MeasureTheory.eLpNorm V q μ)))
(h0 : Φ 0 =ᵐ[μ] h)
(hsmall : 8 * K * (MeasureTheory.eLpNorm h p μ + MeasureTheory.eLpNorm h q μ) ≤ 1)
:
∃ (U : α → E), MeasureTheory.MemLp U p μ ∧ MeasureTheory.MemLp U q μ ∧ Φ U =ᵐ[μ] U
The Picard iteration of a quadratically Lipschitz map for the norm
‖·‖_p + ‖·‖_q, started from its small value at the origin, converges to a
fixed point up to null sets.