Scale invariance of the dimensionless quantities #
This module formalizes the rescaled fields of Definition def:rescaling of
paper/ckn.tex and the transformation law of Lemma lem:scaling-quantities:
at the rescaled base point each of α, β, γ, δ, λ, θ is unchanged
from its value at the original point with the radius scaled by the dilation.
The analytic input is the parabolic change of variables for cylinder integrals
and time-slice essential suprema, together with the elementary algebra of the
exponents. The essential supremum of the velocity L² energy is handled with
the boundedness assumption that makes the transform of an essential supremum
legitimate; every other quantity is unconditional.
The rescaled fields #
The velocity component of the parabolically rescaled solution of Definition
def:rescaling: u^{μ,z₀}(y,s) = μ u(x₀ + μ y, t₀ + μ² s).
Equations
- CKN.rescaleVelocity μ z₀ u w = μ • u (CKN.Foundation.Parabolic.parabolicTranslate z₀.1 z₀.2 (CKN.Foundation.Parabolic.parabolicScale μ w))
Instances For
The pressure component of the parabolically rescaled solution of Definition
def:rescaling: p^{μ,z₀}(y,s) = μ² p(x₀ + μ y, t₀ + μ² s).
Equations
- CKN.rescalePressure μ z₀ p w = μ ^ 2 * p (CKN.Foundation.Parabolic.parabolicTranslate z₀.1 z₀.2 (CKN.Foundation.Parabolic.parabolicScale μ w))
Instances For
The force component of the parabolically rescaled solution of Definition
def:rescaling: f^{μ,z₀}(y,s) = μ³ f(x₀ + μ y, t₀ + μ² s).
Equations
- CKN.rescaleForce μ z₀ f w = μ ^ 3 • f (CKN.Foundation.Parabolic.parabolicTranslate z₀.1 z₀.2 (CKN.Foundation.Parabolic.parabolicScale μ w))
Instances For
The rescaled spatial gradient datum matching rescaleVelocity: the chain
rule gives ∇(u^{μ,z₀}) = μ² (∇u) ∘ T for T(y,s) = (x₀ + μ y, t₀ + μ² s).
Equations
- CKN.rescaleGradient μ z₀ Du w i = μ ^ 2 • Du (CKN.Foundation.Parabolic.parabolicTranslate z₀.1 z₀.2 (CKN.Foundation.Parabolic.parabolicScale μ w)) i
Instances For
The underlying affine map and its Jacobian #
The spatial part y ↦ x + a y of the parabolic rescaling.
Equations
- CKN.spatialAffine a x y = x + a • y
Instances For
The time part s ↦ t + a² s of the parabolic rescaling.
Equations
- CKN.timeAffine a t s = t + a ^ 2 * s
Instances For
The parabolic rescaling map z ↦ (x₀ + μ z₁, t₀ + μ² z₂).
Equations
Instances For
The nonnegative integral over a parabolic cylinder is invariant under the
parabolic rescaling T(y,s) = (x₀ + μ y, t₀ + μ² s) up to the Jacobian factor
μ⁻⁵, matching the change of variables used in Lemma lem:scaling-quantities.
Exponential algebra #
Lemma lem:scaling-quantities, Dirichlet energy: β of the rescaled
solution at the rescaled base point equals β of the original solution at the
original base point with the radius scaled by μ.
Lemma lem:scaling-quantities, velocity L² energy: α of the rescaled
solution at the rescaled base point equals α of the original solution at the
original base point with the radius scaled by μ. The two boundedness
hypotheses are those needed to transform the time-slice essential supremum.
The velocity cubic quantity γ #
Lemma lem:scaling-quantities, velocity cubic quantity: γ of the rescaled
solution at the rescaled base point equals γ of the original solution at the
original base point with the radius scaled by μ.
Lemma lem:scaling-quantities, pressure quantity: δ of the rescaled
solution at the rescaled base point equals δ of the original solution at the
original base point with the radius scaled by μ.
The force quantity λ #
Lemma lem:scaling-quantities, force quantity: λ of the rescaled force at
the rescaled base point equals λ of the original force at the original base
point with the radius scaled by μ, at the same exponent q.
The iteration quantity θ #
Lemma lem:scaling-quantities, iteration quantity: θ of the rescaled
solution at the rescaled base point equals θ of the original solution at the
original base point with the radius scaled by μ, as the sum of the rescaled
α, β and δ.