The physical dilation f(x) ↦ ell*f(x/ell), including actual spatial derivatives and their genuine Banach-valued L² norms.

theorem EulerPhysicalL2Scaling.lpNorm_sq_integral {V : Type u_1} [NormedAddCommGroup V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2 = ∫ (x : EulerSmoothLimit.Space), ‖f x‖ ^ 2

theorem EulerPhysicalL2Scaling.lpNorm_inv_dilation_sq {V : Type u_1} [NormedAddCommGroup V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (ell : ℝ) (hell : 0 < ell) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => f (ell⁻¹ • x)) 2 MeasureTheory.volume ^ 2 = ell ^ 3 * MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

theorem EulerPhysicalL2Scaling.lpNorm_inv_dilation {V : Type u_1} [NormedAddCommGroup V] (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (ell : ℝ) (hell : 0 < ell) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => f (ell⁻¹ • x)) 2 MeasureTheory.volume = √(ell ^ 3) * MeasureTheory.lpNorm f 2 MeasureTheory.volume

noncomputable def EulerPhysicalL2Scaling.scale {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (f : EulerSmoothLimit.Space → V) : EulerSmoothLimit.Space → V

Scale, defined pointwise by ell • f (ell⁻¹ • x).

Equations

• EulerPhysicalL2Scaling.scale ell f x = ell • f (ell⁻¹ • x)

theorem EulerPhysicalL2Scaling.scale_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (scale ell f)

theorem EulerPhysicalL2Scaling.iteratedFDeriv_scale {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : EulerSmoothLimit.Space) : iteratedFDeriv ℝ n (scale ell f) x = (ell * ell⁻¹ ^ n) • iteratedFDeriv ℝ n f (ell⁻¹ • x)

theorem EulerPhysicalL2Scaling.scale_jet_memLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (hn : MeasureTheory.MemLp (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (scale ell f)) 2 MeasureTheory.volume

theorem EulerPhysicalL2Scaling.lpNorm_scale_jet {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (hn : MeasureTheory.MemLp (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume) : MeasureTheory.lpNorm (iteratedFDeriv ℝ n (scale ell f)) 2 MeasureTheory.volume = ell * √(ell ^ 3) * ell⁻¹ ^ n * MeasureTheory.lpNorm (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume

theorem EulerPhysicalL2Scaling.lpNorm_scale_jet_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (hn : MeasureTheory.MemLp (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume) : MeasureTheory.lpNorm (iteratedFDeriv ℝ n (scale ell f)) 2 MeasureTheory.volume ≤ ell⁻¹ ^ n * MeasureTheory.lpNorm (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume