Uniform jets of the actual current physical chart

Only the transverse normalized coordinates are restricted to a fixed annulus. The slow, angular, and free auxiliary coordinates need no bound for the positive jets of the chart map. Native coefficients need smoothness only on a neighborhood of the evaluation point.

@[reducible, inline]

abbrev NavierStokes.CurrentPhysicalChartJets.LiftPoint : Type

Lift point: an abbreviation for PhysicalWaveSum.LiftPoint.

Equations

• NavierStokes.CurrentPhysicalChartJets.LiftPoint = NavierStokes.PhysicalWaveSum.LiftPoint

@[reducible, inline]

abbrev NavierStokes.CurrentPhysicalChartJets.Plane : Type

Plane: an abbreviation for PhysicalGraphBounds.Plane.

Equations

• NavierStokes.CurrentPhysicalChartJets.Plane = NavierStokes.PhysicalGraphBounds.Plane

@[reducible, inline]

abbrev NavierStokes.CurrentPhysicalChartJets.Native : Type

Native: an abbreviation for PhysicalParticularWave.WaveSpace.

Equations

• NavierStokes.CurrentPhysicalChartJets.Native = NavierStokes.PhysicalParticularWave.WaveSpace

@[reducible, inline]

abbrev NavierStokes.CurrentPhysicalChartJets.ComplexVector : Type

Complex vector: an abbreviation for HarmonicCalculus.ComplexVector.

Equations

• NavierStokes.CurrentPhysicalChartJets.ComplexVector = NavierStokes.HarmonicCalculus.ComplexVector

noncomputable def NavierStokes.CurrentPhysicalChartJets.chartMap (a : ℝ) (j : PolarCharts.Index) : LiftPoint → Native

The actual polar lift followed by the solver's fixed coordinate order.

Equations

• NavierStokes.CurrentPhysicalChartJets.chartMap a j x = NavierStokes.PhysicalParticularWave.waveEquiv (NavierStokes.ActualSignedPhysicalData.cylinderAt a j x)

noncomputable def NavierStokes.CurrentPhysicalChartJets.polarPart : Plane →L[ℝ] Native

Only the radial and angular entries depend on the nonlinear polar map.

Equations

• NavierStokes.CurrentPhysicalChartJets.polarPart = (((ContinuousLinearMap.fst ℝ ℝ ℝ).prod 0).prod (ContinuousLinearMap.snd ℝ ℝ ℝ)).prod 0

noncomputable def NavierStokes.CurrentPhysicalChartJets.reversePlane : Plane →L[ℝ] Plane

Reverse plane, given by (ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ).

Equations

• NavierStokes.CurrentPhysicalChartJets.reversePlane = (ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ)

noncomputable def NavierStokes.CurrentPhysicalChartJets.freePart : LiftPoint →L[ℝ] Native

The free coordinates are copied by a bounded linear map.

Equations

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

theorem NavierStokes.CurrentPhysicalChartJets.norm_polarPart_le : ‖polarPart‖ ≤ 1

theorem NavierStokes.CurrentPhysicalChartJets.norm_freePart_le : ‖freePart‖ ≤ 1

theorem NavierStokes.CurrentPhysicalChartJets.chartMap_decomposition (a : ℝ) (j : PolarCharts.Index) : chartMap a j = fun (x : PhysicalGraphBounds.LiftPoint) => polarPart (PolarCharts.chart a j (PhysicalGraphBounds.liftXY x)) + freePart x

theorem NavierStokes.CurrentPhysicalChartJets.chartMap_smooth {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) : ContDiff ℝ (↑⊤) (chartMap a j)

theorem NavierStokes.CurrentPhysicalChartJets.chartMap_positive_jets_ball {a : ℝ} (ha : 0 < a) (b : ℝ) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : PolarCharts.Index) (x : LiftPoint), PhysicalGraphBounds.liftXY x ∈ Metric.closedBall 0 b → ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k (chartMap a j) x‖ ≤ B

One constant bounds all positive map jets on the transverse ball, uniformly in all four charts and every unbounded free coordinate.

theorem NavierStokes.CurrentPhysicalChartJets.chartMap_positive_jets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ (j : PolarCharts.Index), ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k (chartMap a j) x‖ ≤ B

theorem NavierStokes.CurrentPhysicalChartJets.composition_smoothNear {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) {j : PolarCharts.Index} {x : LiftPoint} {f : Native → E} (hf : LocalPhysicalCopyBounds.SmoothNear f (chartMap a j x)) : LocalPhysicalCopyBounds.SmoothNear (f ∘ chartMap a j) x

One native open neighborhood suffices for the pulled-back coefficient.

theorem NavierStokes.CurrentPhysicalChartJets.composition_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) {j : PolarCharts.Index} {x : LiftPoint} {f : Native → E} (m : ℕ) {A B : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hf : LocalPhysicalCopyBounds.SmoothNear f (chartMap a j x)) (hfj : ∀ k ≤ m, ‖iteratedFDeriv ℝ k f (chartMap a j x)‖ ≤ A) (hmap : ∀ (k : ℕ), 1 ≤ k → k ≤ m → ‖iteratedFDeriv ℝ k (chartMap a j) x‖ ≤ B) (k : ℕ) : k ≤ m → ‖iteratedFDeriv ℝ k (f ∘ chartMap a j) x‖ ≤ ↑m.factorial * A * B ^ m

Pointwise finite-jet composition using only the native germ.

theorem NavierStokes.CurrentPhysicalChartJets.composition_jets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℝ} (ha : 0 < a) {b : ℝ} (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (j : PolarCharts.Index), ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ (f : Native → E), LocalPhysicalCopyBounds.SmoothNear f (chartMap a j x) → ∀ (A : ℝ), 0 ≤ A → (∀ k ≤ m, ‖iteratedFDeriv ℝ k f (chartMap a j x)‖ ≤ A) → ∀ k ≤ m, ‖iteratedFDeriv ℝ k (f ∘ chartMap a j) x‖ ≤ C * A

The multiplicative constant is chosen before the chart, point, native coefficient, band, or value of its frozen finite-jet bound.

Compatibility with positive physical radial scaling

theorem NavierStokes.CurrentPhysicalChartJets.chartDomain_smul {a c : ℝ} (hc : 0 < c) (j : PolarCharts.Index) {p : Plane} (hp : p ∈ PolarCharts.chartDomain a j) : c • p ∈ PolarCharts.chartDomain (c * a) j

theorem NavierStokes.CurrentPhysicalChartJets.chart_smul {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (j : PolarCharts.Index) {p : Plane} (hp : p ∈ PolarCharts.chartDomain a j) : PolarCharts.chart (c * a) j (c • p) = (c * (PolarCharts.chart a j p).1, (PolarCharts.chart a j p).2)

On the genuine inverse-chart region, simultaneous scaling of the physical radius and chart padding preserves the exact angular branch.

theorem NavierStokes.CurrentPhysicalChartJets.chart_smul_germ {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (j : PolarCharts.Index) {p : Plane} (hp : p ∈ PolarCharts.chartDomain a j) : (fun (y : Plane) => PolarCharts.chart (c * a) j (c • y)) =ᶠ[nhds p] fun (y : Plane) => (c * (PolarCharts.chart a j y).1, (PolarCharts.chart a j y).2)

The scaling identity holds on an open neighborhood, so it can be used for physical germ and jet comparisons without an angle-branch inference.

The actual Cartesian rotation

noncomputable def NavierStokes.CurrentPhysicalChartJets.rotation (x : LiftPoint) : ComplexVector →L[ℝ] ComplexVector

Rotation, given by CartesianCopySource.rotationMap (PhysicalGraphBounds.liftXY x).

Equations

• NavierStokes.CurrentPhysicalChartJets.rotation x = NavierStokes.CartesianCopySource.rotationMap (NavierStokes.PhysicalGraphBounds.liftXY x)

theorem NavierStokes.CurrentPhysicalChartJets.rotation_smooth {a b : ℝ} (ha : 0 < a) : ContDiffOn ℝ (↑⊤) rotation (PhysicalClassBounds.cylindricalDomain a b)

theorem NavierStokes.CurrentPhysicalChartJets.rotation_smoothNear {a b : ℝ} (ha : 0 < a) {x : LiftPoint} (hx : x ∈ PhysicalClassBounds.cylindricalDomain a b) : LocalPhysicalCopyBounds.SmoothNear rotation x

theorem NavierStokes.CurrentPhysicalChartJets.rotation_jets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ k ≤ m, ‖iteratedFDeriv ℝ k rotation x‖ ≤ C

These are full jets, including order zero, of the literal rotation operator. The same constant works for every chart and free coordinate.

theorem NavierStokes.CurrentPhysicalChartJets.rotationMap_smul {c : ℝ} (hc : 0 < c) (p : Plane) : CartesianCopySource.rotationMap (c • p) = CartesianCopySource.rotationMap p

Positive radial rescaling leaves the actual Cartesian rotation fixed, including at its totalized zero input.

noncomputable def NavierStokes.CurrentPhysicalChartJets.rotated (a : ℝ) (j : PolarCharts.Index) (f : Native → ComplexVector) (x : LiftPoint) : ComplexVector

Rotate a native vector coefficient after pulling it into the actual normalized Cartesian lift.

Equations

• NavierStokes.CurrentPhysicalChartJets.rotated a j f x = (NavierStokes.CurrentPhysicalChartJets.rotation x) (f (NavierStokes.CurrentPhysicalChartJets.chartMap a j x))

theorem NavierStokes.CurrentPhysicalChartJets.rotated_smoothNear {a b : ℝ} (ha : 0 < a) {j : PolarCharts.Index} {x : LiftPoint} (hx : x ∈ PhysicalClassBounds.cylindricalDomain a b) {f : Native → ComplexVector} (hf : LocalPhysicalCopyBounds.SmoothNear f (chartMap a j x)) : LocalPhysicalCopyBounds.SmoothNear (rotated a j f) x

theorem NavierStokes.CurrentPhysicalChartJets.rotated_composition_jets {a b : ℝ} (ha : 0 < a) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (j : PolarCharts.Index), ∀ x ∈ PhysicalClassBounds.cylindricalDomain a b, ∀ (f : Native → ComplexVector), LocalPhysicalCopyBounds.SmoothNear f (chartMap a j x) → ∀ (A : ℝ), 0 ≤ A → (∀ k ≤ m, ‖iteratedFDeriv ℝ k f (chartMap a j x)‖ ≤ A) → ∀ k ≤ m, ‖iteratedFDeriv ℝ k (rotated a j f) x‖ ≤ C * A

Local composition and the full Leibniz estimate give a uniform bound for the actual rotated coefficient, including order zero. The constant is independent of every band or label entering the native finite-jet bound.

The fixed Cartesian realification

theorem NavierStokes.CurrentPhysicalChartJets.realVector_norm_le (z : ComplexVector) : ‖PhysicalCurlCovariance.realVector z‖ ≤ 3 * ‖z‖

noncomputable def NavierStokes.CurrentPhysicalChartJets.realVectorCLM : ComplexVector →L[ℝ] ProblemStatement.Space

The literal real-vector constructor is a fixed bounded linear map. This provides the final codomain conversion for physical vector modes.

Equations

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

@[simp]

theorem NavierStokes.CurrentPhysicalChartJets.realVectorCLM_apply (z : ComplexVector) : realVectorCLM z = PhysicalCurlCovariance.realVector z

theorem NavierStokes.CurrentPhysicalChartJets.norm_realVectorCLM_le : ‖realVectorCLM‖ ≤ 3