Hölder-seminorm bookkeeping for the analytic case of r.LeBron.2 #
Monotonicity in the constant and in the exponent, extraction of the seminorm from
HolderTimeL2Le, the L² triangle inequality for L² slices, and the telescoping chain lemma.
theorem
AVenhance.Infra.FullTheorem.IsHolderTimeL2.mono_const
{μ H H' : ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(h : IsHolderTimeL2 μ H θ)
(hH : H ≤ H')
:
IsHolderTimeL2 μ H' θ
theorem
AVenhance.Infra.FullTheorem.IsHolderTimeL2.mono_exp
{μ μ' H : ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hμ' : 0 < μ')
(hμ : μ' ≤ μ)
(hH : 0 ≤ H)
(h : IsHolderTimeL2 μ H θ)
:
IsHolderTimeL2 μ' H θ
theorem
AVenhance.Infra.FullTheorem.holderTimeL2Le_isHolder
{μ H : ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(h : HolderTimeL2Le μ H θ)
:
IsHolderTimeL2 μ H θ
theorem
AVenhance.Infra.FullTheorem.sqrt_l2NormSq_sub_le_memL2
{f g : Homogenization.Vec 2 → ℝ}
(hf : Homogenization.MemL2On unitCube f)
(hg : Homogenization.MemL2On unitCube g)
:
Triangle inequality for a sum of two L² functions.
theorem
AVenhance.Infra.FullTheorem.chain_holder
{f : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{μ A : ℝ}
{c : ℕ → ℝ}
{n₀ : ℕ}
(hbase : IsHolderTimeL2 μ A (f n₀))
(M : ℕ)
:
n₀ ≤ M →
(∀ (n : ℕ), n₀ ≤ n → n ≤ M → ∀ t ∈ Set.Icc 0 1, Continuous (f n t)) →
(∀ (n : ℕ),
n₀ < n → n ≤ M → IsHolderTimeL2 μ (c n) fun (t : ℝ) (x : Homogenization.Vec 2) => f n t x - f (n - 1) t x) →
IsHolderTimeL2 μ (A + ∑ n ∈ Finset.Ioc n₀ M, c n) (f M)
Telescoping chain: a base Hölder bound at n₀ plus Hölder bounds for the increments.
theorem
AVenhance.Infra.FullTheorem.holder_split
{μ H₁ H₂ : ℝ}
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
(hθ : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (θ t))
(hM : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (θM t))
(h1 : IsHolderTimeL2 μ H₁ θM)
(h2 : IsHolderTimeL2 μ H₂ fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x)
:
IsHolderTimeL2 μ (H₁ + H₂) θ
Splitting θ = θ_M + (θ − θ_M) in the Hölder seminorm.