Cartesian source classes for actual native copies

The cylindrical radius and the Cartesian rotation are evaluated directly on the lift. Their derivatives are bounded on a fixed annulus, and the original flat weight is pulled back exactly.

@[reducible, inline]

abbrev NavierStokes.CartesianCopySource.Plane : Type

Plane: an abbreviation for PhysicalGraphBounds.Plane.

Equations

• NavierStokes.CartesianCopySource.Plane = NavierStokes.PhysicalGraphBounds.Plane

@[reducible, inline]

abbrev NavierStokes.CartesianCopySource.LiftPoint : Type

Lift point: an abbreviation for PhysicalWaveSum.LiftPoint.

Equations

• NavierStokes.CartesianCopySource.LiftPoint = NavierStokes.PhysicalWaveSum.LiftPoint

@[reducible, inline]

abbrev NavierStokes.CartesianCopySource.Native : Type

Native: an abbreviation for PhysicalClassBounds.CylindricalPoint.

Equations

• NavierStokes.CartesianCopySource.Native = NavierStokes.PhysicalClassBounds.CylindricalPoint

@[reducible, inline]

abbrev NavierStokes.CartesianCopySource.ComplexVector : Type

Complex vector: an abbreviation for HarmonicCalculus.ComplexVector.

Equations

• NavierStokes.CartesianCopySource.ComplexVector = NavierStokes.HarmonicCalculus.ComplexVector

theorem NavierStokes.CartesianCopySource.cylindricalMap_continuous : Continuous PhysicalClassBounds.cylindricalMap

noncomputable def NavierStokes.CartesianCopySource.pullStrip (s : WeightedClasses.StripData Native) (a b : ℝ) (ha : 0 < a) : WeightedClasses.StripData LiftPoint

Restriction to a padded annulus and the genuine native domain. The weight, edge distance, viscosity and slow scales are unchanged by pullback.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NavierStokes.CartesianCopySource.pullStrip_zeta (s : WeightedClasses.StripData Native) (a b : ℝ) (ha : 0 < a) (x : LiftPoint) : (pullStrip s a b ha).zeta x = s.zeta (PhysicalClassBounds.cylindricalMap x)

@[simp]

theorem NavierStokes.CartesianCopySource.pullStrip_growth (s : WeightedClasses.StripData Native) (a b : ℝ) (ha : 0 < a) (n : ℕ) (x : LiftPoint) : (pullStrip s a b ha).growth n x = s.growth n (PhysicalClassBounds.cylindricalMap x)

theorem NavierStokes.CartesianCopySource.uniform_pullback {ι : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData Native} {w : ι → ℕ → Native → ℝ} {f : ι → ℕ → Native → E} {α a b : ℝ} (ha : 0 < a) (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (pullStrip s a b ha) (fun (l : ι) (n : ℕ) (x : LiftPoint) => w l n (PhysicalClassBounds.cylindricalMap x)) α fun (l : ι) (n : ℕ) (x : LiftPoint) => f l n (PhysicalClassBounds.cylindricalMap x)

Constants are chosen before labels, bands and copies. No positive minimum of the flat weight occurs in this composition argument.

theorem NavierStokes.CartesianCopySource.flatGeometry_pullback {s : WeightedClasses.StripData Native} {a b : ℝ} (ha : 0 < a) {cL cR L : ℝ} {ρ : Native → ℝ} (hflat : PhysicalClassBounds.FlatGeometry s cL cR L ρ) : PhysicalClassBounds.FlatGeometry (pullStrip s a b ha) cL cR L fun (x : LiftPoint) => ρ (PhysicalClassBounds.cylindricalMap x)

theorem NavierStokes.CartesianCopySource.sourceBounds_pullback {ι : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData Native} {w : ι → ℕ → Native → ℝ} {f : ι → ℕ → Native → E} {α a b : ℝ} (ha : 0 < a) {h : ℝ} (hf : LocalPhysicalCopyBounds.LocalSourceBounds s h α w f) : LocalPhysicalCopyBounds.LocalSourceBounds (pullStrip s a b ha) h α (fun (l : ι) (n : ℕ) (x : LiftPoint) => w l n (PhysicalClassBounds.cylindricalMap x)) fun (l : ι) (n : ℕ) (x : LiftPoint) => f l n (PhysicalClassBounds.cylindricalMap x)

Actual Cartesian rotation

noncomputable def NavierStokes.CartesianCopySource.horizontal : ComplexVector →L[ℝ] ComplexVector

Horizontal, given by ContinuousLinearMap.pi ![ContinuousLinearMap.proj 0, ContinuousLinearMap.proj 1, 0].

Equations

• NavierStokes.CartesianCopySource.horizontal = ContinuousLinearMap.pi ![ContinuousLinearMap.proj 0, ContinuousLinearMap.proj 1, 0]

noncomputable def NavierStokes.CartesianCopySource.connection : ComplexVector →L[ℝ] ComplexVector

Connection, given by ContinuousLinearMap.pi ![-ContinuousLinearMap.proj 1, ContinuousLinearMap.proj 0, 0].

Equations

• NavierStokes.CartesianCopySource.connection = ContinuousLinearMap.pi ![-ContinuousLinearMap.proj 1, ContinuousLinearMap.proj 0, 0]

noncomputable def NavierStokes.CartesianCopySource.vertical : ComplexVector →L[ℝ] ComplexVector

Vertical, given by ContinuousLinearMap.pi ![0, 0, ContinuousLinearMap.proj 2].

Equations

• NavierStokes.CartesianCopySource.vertical = ContinuousLinearMap.pi ![0, 0, ContinuousLinearMap.proj 2]

noncomputable def NavierStokes.CartesianCopySource.rotationMap (y : Plane) : ComplexVector →L[ℝ] ComplexVector

Rotation map, given by (y.1 / cartesianRadius y) • horizontal + (y.2 / cartesianRadius y) • connection + vertical.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CartesianCopySource.rotationMap_apply (y : Plane) (v : ComplexVector) : (rotationMap y) v = ![(y.1 / PhysicalClassBounds.cartesianRadius y) • v 0 - (y.2 / PhysicalClassBounds.cartesianRadius y) • v 1, (y.2 / PhysicalClassBounds.cartesianRadius y) • v 0 + (y.1 / PhysicalClassBounds.cartesianRadius y) • v 1, v 2]

theorem NavierStokes.CartesianCopySource.rotationMap_smooth : ContDiffOn ℝ (↑⊤) rotationMap {y : Plane | y ≠ 0}

theorem NavierStokes.CartesianCopySource.rotationMap_jets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ j ≤ m, ‖iteratedFDeriv ℝ j (fun (y : PhysicalGraphBounds.LiftPoint) => rotationMap (PhysicalGraphBounds.liftXY y)) x‖ ≤ C

Actual all-order rotation jets have uniform bounds on the padded annulus, independently of every slow and auxiliary coordinate.

theorem NavierStokes.CartesianCopySource.rotation_uniform {ι : Type u_1} (s : WeightedClasses.StripData Native) {a b : ℝ} (ha : 0 < a) : LabelSumBounds.UniformClass (pullStrip s a b ha) (fun (x : ι) (x_1 : ℕ) (x_2 : LiftPoint) => 1) 0 fun (x : ι) (x_1 : ℕ) (x_2 : LiftPoint) => rotationMap (PhysicalGraphBounds.liftXY x_2)

noncomputable def NavierStokes.CartesianCopySource.rotatedSource {ι : Type u_1} (f : ι → ℕ → Native → ComplexVector) (l : ι) (n : ℕ) (x : LiftPoint) : ComplexVector

Rotated source, given by rotationMap (PhysicalGraphBounds.liftXY x) (f l n (cylindricalMap x)).

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.CartesianCopySource.uniform_rotated {ι : Type u_1} {s : WeightedClasses.StripData Native} {w : ι → ℕ → Native → ℝ} {f : ι → ℕ → Native → ComplexVector} {α a b : ℝ} (ha : 0 < a) (hf : LabelSumBounds.UniformClass s w α f) : LabelSumBounds.UniformClass (pullStrip s a b ha) (fun (l : ι) (n : ℕ) (x : LiftPoint) => w l n (PhysicalClassBounds.cylindricalMap x)) α (rotatedSource f)

theorem NavierStokes.CartesianCopySource.sourceBounds_rotated {ι : Type u_1} {s : WeightedClasses.StripData Native} {w : ι → ℕ → Native → ℝ} {f : ι → ℕ → Native → ComplexVector} {α h a b : ℝ} (ha : 0 < a) (hf : LocalPhysicalCopyBounds.LocalSourceBounds s h α w f) : LocalPhysicalCopyBounds.LocalSourceBounds (pullStrip s a b ha) h α (fun (l : ι) (n : ℕ) (x : LiftPoint) => w l n (PhysicalClassBounds.cylindricalMap x)) (rotatedSource f)

theorem NavierStokes.CartesianCopySource.sourceBounds_rotated_component {ι : Type u_1} {s : WeightedClasses.StripData Native} {w : ι → ℕ → Native → ℝ} {f : ι → ℕ → Native → ComplexVector} {α h a b : ℝ} (ha : 0 < a) (hf : LocalPhysicalCopyBounds.LocalSourceBounds s h α w f) (i : Fin 3) : LocalPhysicalCopyBounds.LocalSourceBounds (pullStrip s a b ha) h α (fun (l : ι) (n : ℕ) (x : LiftPoint) => w l n (PhysicalClassBounds.cylindricalMap x)) fun (l : ι) (n : ℕ) (x : LiftPoint) => rotatedSource f l n x i