Uniform stripped jets on a common cover

The input of the copy solve is evaluated on the common torus. The two actual argument maps below include the integration time as a variable. Their affine derivatives, the native time scale, and adjacent-band changes give estimates whose constants precede the band, copy, and source. No native periodicity of the source is used.

@[reducible, inline]

abbrev NavierStokes.CommonCoverClass.CCS : Type

CCS: an abbreviation for CommonCoverSolve.Geometry.

Equations

• NavierStokes.CommonCoverClass.CCS = NavierStokes.CommonCoverSolve.Geometry

def NavierStokes.CommonCoverClass.EnvelopeJets {X V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] (m : ℕ) (f : X → V) (envelope : X → ℝ) : Prop

A point-dependent bound on a finite prefix of actual Fréchet jets.

Equations

• NavierStokes.CommonCoverClass.EnvelopeJets m f envelope = ∀ j ≤ m, ∀ (x : X), ‖iteratedFDeriv ℝ j f x‖ ≤ envelope x

theorem NavierStokes.CommonCoverClass.EnvelopeJets.nonneg {X V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {m : ℕ} {f : X → V} {e : X → ℝ} (hf : EnvelopeJets m f e) (x : X) : 0 ≤ e x

theorem NavierStokes.CommonCoverClass.EnvelopeJets.mono {X V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] {m : ℕ} {f : X → V} {e e' : X → ℝ} (hf : EnvelopeJets m f e) (he : ∀ (x : X), e x ≤ e' x) : EnvelopeJets m f e'

theorem NavierStokes.CommonCoverClass.affine_jet_bound {X Y V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Y → V} (hf : ContDiff ℝ (↑⊤) f) (L : X →L[ℝ] Y) (c : Y) {K : ℝ} (hK : 1 ≤ K) (hL : ‖L‖ ≤ K) (m : ℕ) (x : X) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (c + L x)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (z : X) => f (c + L z)) x‖ ≤ A * K ^ m

theorem NavierStokes.CommonCoverClass.EnvelopeJets.affine {X Y V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {m : ℕ} {f : Y → V} {e : Y → ℝ} (hb : EnvelopeJets m f e) (hf : ContDiff ℝ (↑⊤) f) (L : X →L[ℝ] Y) (c : Y) {K : ℝ} (hK : 1 ≤ K) (hL : ‖L‖ ≤ K) : EnvelopeJets m (fun (x : X) => f (c + L x)) fun (x : X) => e (c + L x) * K ^ m

theorem NavierStokes.CommonCoverClass.clm_apply_jet_bound {X V W : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {f : X → V →L[ℝ] W} {g : X → V} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (m : ℕ) (x : X) {A B : ℝ} (hA : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f x‖ ≤ A) (hB : ∀ j ≤ m, ‖iteratedFDeriv ℝ j g x‖ ≤ B) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (y : X) => (f y) (g y)) x‖ ≤ 2 ^ m * A * B

The weight is evaluated at the same point in both factors; it need not be differentiated in this bound.

theorem NavierStokes.CommonCoverClass.EnvelopeJets.clm_apply {X V W : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {m : ℕ} {f : X → V →L[ℝ] W} {g : X → V} {A B : X → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hA : EnvelopeJets m f A) (hB : EnvelopeJets m g B) : EnvelopeJets m (fun (x : X) => (f x) (g x)) fun (x : X) => 2 ^ m * A x * B x

@[reducible, inline]

abbrev NavierStokes.CommonCoverClass.Joint (P : Type) : Type

Joint slow/common-coordinate/integration-time space.

Equations

• NavierStokes.CommonCoverClass.Joint P = ((P × NavierStokes.TorusInverse.Plane) × ℝ)

noncomputable def NavierStokes.CommonCoverClass.nativeArgument {P : Type} (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : P × TorusInverse.Plane

Native argument, given by (w.1.1, ((g.coordinates k w.1.2).1, w.2)).

Equations

• NavierStokes.CommonCoverClass.nativeArgument g k w = (w.1.1, (NavierStokes.CommonCoverSolve.Geometry.coordinates g k w.1.2).1, w.2)

noncomputable def NavierStokes.CommonCoverClass.sourceArgument {P : Type} (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : P × TorusInverse.Plane

Source argument, given by (w.1.1, g.path k w.1.2 w.2).

Equations

• NavierStokes.CommonCoverClass.sourceArgument g k w = (w.1.1, NavierStokes.CommonCoverSolve.Geometry.path g k w.1.2 w.2)

noncomputable def NavierStokes.CommonCoverClass.nativeLinear (P : Type) [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : Joint P →L[ℝ] P × TorusInverse.Plane

Native linear as an element of Joint P →L[ℝ] P × Plane.

Equations

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

noncomputable def NavierStokes.CommonCoverClass.sourceLinear (P : Type) [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : Joint P →L[ℝ] P × TorusInverse.Plane

Source linear as an element of Joint P →L[ℝ] P × Plane.

Equations

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

@[simp]

theorem NavierStokes.CommonCoverClass.nativeLinear_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (w : Joint P) : (nativeLinear P g) w = (w.1.1, ((CommonCoverSolve.Geometry.coordinateLinear g) w.1.2).1, w.2)

@[simp]

theorem NavierStokes.CommonCoverClass.sourceLinear_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (w : Joint P) : (sourceLinear P g) w = (w.1.1, (CommonCoverSolve.Geometry.pointLinear g) (((CommonCoverSolve.Geometry.coordinateLinear g) w.1.2).1, w.2))

theorem NavierStokes.CommonCoverClass.nativeArgument_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : nativeArgument g k w = nativeArgument g k 0 + (nativeLinear P g) w

theorem NavierStokes.CommonCoverClass.sourceArgument_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : sourceArgument g k w = sourceArgument g k 0 + (sourceLinear P g) w

theorem NavierStokes.CommonCoverClass.nativeArgument_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (nativeArgument g k)

theorem NavierStokes.CommonCoverClass.sourceArgument_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (sourceArgument g k)

noncomputable def NavierStokes.CommonCoverClass.argumentCost (g : CCS) : ℝ

One common affine cost for both maps. Its value is independent of the copy index and of the slow parameter space.

Equations

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

theorem NavierStokes.CommonCoverClass.one_le_argumentCost (g : CCS) : 1 ≤ argumentCost g

theorem NavierStokes.CommonCoverClass.norm_nativeLinear_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : ‖nativeLinear P g‖ ≤ argumentCost g

theorem NavierStokes.CommonCoverClass.norm_sourceLinear_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : ‖sourceLinear P g‖ ≤ argumentCost g

theorem NavierStokes.CommonCoverClass.nativeArgument_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (g : CCS) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Joint P) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (nativeArgument g k w)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (z : Joint P) => f (nativeArgument g k z)) w‖ ≤ A * argumentCost g ^ m

theorem NavierStokes.CommonCoverClass.sourceArgument_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (g : CCS) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Joint P) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (sourceArgument g k w)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (z : Joint P) => f (sourceArgument g k z)) w‖ ≤ A * argumentCost g ^ m

@[simp]

theorem NavierStokes.CommonCoverClass.sourceArgument_slow {P : Type} (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : (sourceArgument g k w).1 = w.1.1

@[simp]

theorem NavierStokes.CommonCoverClass.nativeArgument_slow {P : Type} (g : CCS) (k : TorusInverse.Frequency) (w : Joint P) : (nativeArgument g k w).1 = w.1.1

noncomputable def NavierStokes.CommonCoverClass.scaledBasis (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (ci : ℝ) (hci : ci ≠ 0) : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

The fixed native basis has columns v_r,v_t; only the second column is multiplied by the actual time coefficient.

Equations

• NavierStokes.CommonCoverClass.scaledBasis B ci hci = (NavierStokes.TorusAverages.transverseChart ci hci).trans B

theorem NavierStokes.CommonCoverClass.scaledBasis_apply (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (ci : ℝ) (hci : ci ≠ 0) (z : TorusInverse.Plane) : (scaledBasis B ci hci) z = B (z.1, ci * z.2)

theorem NavierStokes.CommonCoverClass.scaledBasis_transverse (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (ci : ℝ) (hci : ci ≠ 0) : (scaledBasis B ci hci) (0, 1) = ci • B (0, 1)

theorem NavierStokes.CommonCoverClass.norm_transverseChart_le {ci : ℝ} (hci : ci ≠ 0) (habs : |ci| ≤ 1) : ‖↑(TorusAverages.transverseChart ci hci)‖ ≤ 1

theorem NavierStokes.CommonCoverClass.norm_inverse_transverseChart_le (ci : ℝ) (hci : ci ≠ 0) : ‖↑(TorusAverages.transverseChart ci hci).symm‖ ≤ 1 + |ci⁻¹|

theorem NavierStokes.CommonCoverClass.norm_scaledBasis_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {ci : ℝ} (hci : ci ≠ 0) (habs : |ci| ≤ 1) : ‖↑(scaledBasis B ci hci)‖ ≤ ‖↑B‖

theorem NavierStokes.CommonCoverClass.norm_inverse_scaledBasis_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (ci : ℝ) (hci : ci ≠ 0) : ‖↑(scaledBasis B ci hci).symm‖ ≤ (1 + |ci⁻¹|) * ‖↑B.symm‖

noncomputable def NavierStokes.CommonCoverClass.bandGeometry (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane) : CCS

Band geometry, bundling gap, basis, center.

Equations

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

theorem NavierStokes.CommonCoverClass.bandGeometry_path (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : CommonCoverSolve.Geometry.path (bandGeometry B h n gap center) k Y s = Y + (CommonCoverSolve.coverPower gap).symm ((ChartScales.timeCoefficient h n * (s - (CommonCoverSolve.Geometry.coordinates (bandGeometry B h n gap center) k Y).2)) • B (0, 1))

noncomputable def NavierStokes.CommonCoverClass.geometryCost (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (D : ℕ) : ℝ

Geometry cost, constructed using 1.

Equations

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

theorem NavierStokes.CommonCoverClass.geometryCost_one_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (D : ℕ) : 1 ≤ geometryCost B D

noncomputable def NavierStokes.CommonCoverClass.bandArgumentCost (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (D : ℕ) : ℝ

This constant depends on the fixed native basis and the covering-gap budget, and is chosen before the band, center, copy, or source.

Equations

• NavierStokes.CommonCoverClass.bandArgumentCost B D = (1 + NavierStokes.CommonCoverClass.geometryCost B D) ^ 2

theorem NavierStokes.CommonCoverClass.bandArgumentCost_one_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) (D : ℕ) : 1 ≤ bandArgumentCost B D

theorem NavierStokes.CommonCoverClass.bandGeometry_argumentCost_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) : argumentCost (bandGeometry B h n gap center) ≤ bandArgumentCost B D * ChartScales.S n

noncomputable def NavierStokes.CommonCoverClass.currentArgument {P : Type} (g : CCS) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : Joint P

Reinsert the actual current slot time after solving the joint equation.

Equations

• NavierStokes.CommonCoverClass.currentArgument g k p = (p, (NavierStokes.CommonCoverSolve.Geometry.coordinates g k p.2).2)

noncomputable def NavierStokes.CommonCoverClass.currentLinear (P : Type) [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : P × TorusInverse.Plane →L[ℝ] Joint P

Current linear as an element of P × Plane →L[ℝ] Joint P.

Equations

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

@[simp]

theorem NavierStokes.CommonCoverClass.currentLinear_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (p : P × TorusInverse.Plane) : (currentLinear P g) p = (p, ((CommonCoverSolve.Geometry.coordinateLinear g) p.2).2)

theorem NavierStokes.CommonCoverClass.currentArgument_affine {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) (p : P × TorusInverse.Plane) : currentArgument g k p = currentArgument g k 0 + (currentLinear P g) p

theorem NavierStokes.CommonCoverClass.currentArgument_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (currentArgument g k)

theorem NavierStokes.CommonCoverClass.norm_currentLinear_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (g : CCS) : ‖currentLinear P g‖ ≤ argumentCost g

theorem NavierStokes.CommonCoverClass.currentArgument_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (g : CCS) (k : TorusInverse.Frequency) {f : Joint P → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (p : P × TorusInverse.Plane) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (currentArgument g k p)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (q : P × TorusInverse.Plane) => f (currentArgument g k q)) p‖ ≤ A * argumentCost g ^ m

theorem NavierStokes.CommonCoverClass.nativeArgument_band_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Joint P) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (nativeArgument (bandGeometry B h n gap center) k w)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (z : Joint P) => f (nativeArgument (bandGeometry B h n gap center) k z)) w‖ ≤ A * (bandArgumentCost B D * ChartScales.S n) ^ m

theorem NavierStokes.CommonCoverClass.sourceArgument_band_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (w : Joint P) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (sourceArgument (bandGeometry B h n gap center) k w)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (z : Joint P) => f (sourceArgument (bandGeometry B h n gap center) k z)) w‖ ≤ A * (bandArgumentCost B D * ChartScales.S n) ^ m

theorem NavierStokes.CommonCoverClass.currentArgument_band_jet_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) {f : Joint P → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (p : P × TorusInverse.Plane) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (currentArgument (bandGeometry B h n gap center) k p)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (q : P × TorusInverse.Plane) => f (currentArgument (bandGeometry B h n gap center) k q)) p‖ ≤ A * (bandArgumentCost B D * ChartScales.S n) ^ m

theorem NavierStokes.CommonCoverClass.sourceArgument_envelope {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (g : CCS) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) {m : ℕ} {e : P × TorusInverse.Plane → ℝ} (hb : EnvelopeJets m f e) : EnvelopeJets m (fun (z : Joint P) => f (sourceArgument g k z)) fun (z : Joint P) => e (sourceArgument g k z) * argumentCost g ^ m

theorem NavierStokes.CommonCoverClass.nativeArgument_envelope {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (g : CCS) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) {m : ℕ} {e : P × TorusInverse.Plane → ℝ} (hb : EnvelopeJets m f e) : EnvelopeJets m (fun (z : Joint P) => f (nativeArgument g k z)) fun (z : Joint P) => e (nativeArgument g k z) * argumentCost g ^ m

theorem NavierStokes.CommonCoverClass.coefficientAlong_band_jet_bound {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) (hf : ContDiff ℝ (↑⊤) d.coefficient) (m : ℕ) (w : Joint P) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j d.coefficient (nativeArgument (bandGeometry B h n gap center) k w)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (d.coefficientAlong (bandGeometry B h n gap center) k) w‖ ≤ A * (bandArgumentCost B D * ChartScales.S n) ^ m

This is a bound on all joint input jets of the actual ODE coefficient.

theorem NavierStokes.CommonCoverClass.forcingAlong_band_jet_bound {P V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) (hB : ContDiff ℝ (↑⊤) d.forcingMap) (hf : ContDiff ℝ (↑⊤) d.source) (m : ℕ) (w : Joint P) {A C : ℝ} (hA : ∀ j ≤ m, ‖iteratedFDeriv ℝ j d.forcingMap (nativeArgument (bandGeometry B h n gap center) k w)‖ ≤ A) (hC : ∀ j ≤ m, ‖iteratedFDeriv ℝ j d.source (sourceArgument (bandGeometry B h n gap center) k w)‖ ≤ C) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (d.forcingAlong (bandGeometry B h n gap center) k) w‖ ≤ 2 ^ m * A * C * bandArgumentCost B D ^ (2 * m) * ChartScales.S n ^ (2 * m)

Both factors are evaluated at their correct, generally different, arguments. In particular the source is not replaced by a native-periodic one.

theorem NavierStokes.CommonCoverClass.sourceArgument_band_stripped_bound {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) {n gap D : ℕ} (hn : 4 ≤ n) (hd : gap ≤ D) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) {f : P × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) (m p q : ℕ) (A α : ℝ) (edge weight : P → ℝ) (hb : ∀ j ≤ m, ∀ (z : P × TorusInverse.Plane), ‖iteratedFDeriv ℝ j f z‖ ≤ A * ChartScales.epsilon h n ^ α * ChartScales.S n ^ p * edge z.1 ^ q * weight z.1) (j : ℕ) : j ≤ m → ∀ (w : Joint P), ‖iteratedFDeriv ℝ j (fun (z : Joint P) => f (sourceArgument (bandGeometry B h n gap center) k z)) w‖ ≤ A * bandArgumentCost B D ^ m * ChartScales.epsilon h n ^ α * ChartScales.S n ^ (p + m) * edge w.1.1 ^ q * weight w.1.1

Every radial and slow weight is unchanged by the source path. For each requested jet prefix the only change is a fixed additional power of S. This also applies with weight = sqrt(zeta) * P whenever P depends only on the retained slow parameters.

noncomputable def NavierStokes.CommonCoverClass.bandRatio (a : ℝ) (n m : ℕ) : ℝ

The exact ratio (Q_n / Q_m)^a, written without a division.

Equations

• NavierStokes.CommonCoverClass.bandRatio a n m = 2 ^ ((↑m - ↑n) * a)

theorem NavierStokes.CommonCoverClass.bandRatio_pos (a : ℝ) (n m : ℕ) : 0 < bandRatio a n m

theorem NavierStokes.CommonCoverClass.bandRatio_eq_rpow (a : ℝ) (n m : ℕ) : bandRatio a n m = (ChartScales.Q n / ChartScales.Q m) ^ a

theorem NavierStokes.CommonCoverClass.bandRatio_mul_scale (a : ℝ) (n m : ℕ) : bandRatio a n m * ChartScales.Q n ^ (-a) = ChartScales.Q m ^ (-a)

theorem NavierStokes.CommonCoverClass.bandRatio_mul_power (a : ℝ) (n m : ℕ) : bandRatio a n m * ChartScales.Q m ^ a = ChartScales.Q n ^ a

theorem NavierStokes.CommonCoverClass.bandRatio_le (a : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : bandRatio a n m ≤ 2 ^ (4 * |a|)

theorem NavierStokes.CommonCoverClass.epsilon_power_transfer (h α : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ChartScales.epsilon h n ^ α ≤ 2 ^ (4 * |h * α|) * ChartScales.epsilon h m ^ α

Transfer of the actual small-scale factor across overlapping bands. The exponent is identical on both sides.

theorem NavierStokes.CommonCoverClass.slow_scale_transfer {n m : ℕ} (hm : 1 ≤ m) (hnm : n ≤ m + 4) : ChartScales.S n ≤ 25 * ChartScales.S m

theorem NavierStokes.CommonCoverClass.slow_power_transfer {n m : ℕ} (hm : 1 ≤ m) (hnm : n ≤ m + 4) (p : ℕ) : ChartScales.S n ^ p ≤ 25 ^ p * ChartScales.S m ^ p

@[reducible, inline]

abbrev NavierStokes.CommonCoverClass.SlowPoint : Type

Slow point: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.CommonCoverClass.SlowPoint = (ℝ × ℝ × ℝ)

noncomputable def NavierStokes.CommonCoverClass.bandChart (D : ℝ) (n m : ℕ) : SlowPoint →L[ℝ] SlowPoint

Actual (R,Z,T) chart change from band n to band m.

Equations

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

@[simp]

theorem NavierStokes.CommonCoverClass.bandChart_apply (D : ℝ) (n m : ℕ) (x : SlowPoint) : (bandChart D n m) x = (bandRatio (1 / 2) n m * x.1, bandRatio D n m * x.2.1, bandRatio 1 n m * x.2.2)

theorem NavierStokes.CommonCoverClass.bandChart_formula (D : ℝ) (n m : ℕ) (x : SlowPoint) : (bandChart D n m) x = ((ChartScales.Q n / ChartScales.Q m) ^ (1 / 2) * x.1, (ChartScales.Q n / ChartScales.Q m) ^ D * x.2.1, ChartScales.Q n / ChartScales.Q m * x.2.2)

noncomputable def NavierStokes.CommonCoverClass.normalizedSlowChart (D : ℝ) (n : ℕ) (x : SlowPoint) : SlowPoint

Normalized slow chart, given by (ChartScales.Q n ^ (-(1 / 2 : ℝ)) * x.1, (ChartScales.Q n ^ (-D) * x.2.1, ChartScales.Q n ^ (-1 : ℝ) * x.2.2)).

Equations

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

theorem NavierStokes.CommonCoverClass.bandChart_normalizedSlowChart (D : ℝ) (n m : ℕ) (x : SlowPoint) : (bandChart D n m) (normalizedSlowChart D n x) = normalizedSlowChart D m x

noncomputable def NavierStokes.CommonCoverClass.chartCost (D : ℝ) : ℝ

Chart cost, given by 1 + (2 : ℝ) ^ (4 * (1 + |D|)).

Equations

• NavierStokes.CommonCoverClass.chartCost D = 1 + 2 ^ (4 * (1 + |D|))

theorem NavierStokes.CommonCoverClass.chartCost_one_le (D : ℝ) : 1 ≤ chartCost D

theorem NavierStokes.CommonCoverClass.bandRatio_le_chartCost {D a : ℝ} (ha : |a| ≤ 1 + |D|) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : bandRatio a n m ≤ chartCost D

theorem NavierStokes.CommonCoverClass.norm_bandChart_le (D : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ‖bandChart D n m‖ ≤ chartCost D

theorem NavierStokes.CommonCoverClass.bandChart_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SlowPoint → V} (hf : ContDiff ℝ (↑⊤) f) (D : ℝ) {n m : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (r : ℕ) (x : SlowPoint) {A : ℝ} (hb : ∀ j ≤ r, ‖iteratedFDeriv ℝ j f ((bandChart D n m) x)‖ ≤ A) (j : ℕ) : j ≤ r → ‖iteratedFDeriv ℝ j (fun (y : SlowPoint) => f ((bandChart D n m) y)) x‖ ≤ A * chartCost D ^ r

noncomputable def NavierStokes.CommonCoverClass.commonIndex (h : ℝ) (n m : ℕ) : ℕ

Coarsest of a pair of simultaneously active levels.

Equations

• NavierStokes.CommonCoverClass.commonIndex h n m = min (NavierStokes.ChartScales.nativeIndex h n) (NavierStokes.ChartScales.nativeIndex h m)

theorem NavierStokes.CommonCoverClass.commonIndex_gap_le (h : ℝ) (hh : 0 ≤ h) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) : ChartScales.nativeIndex h n - commonIndex h n m ≤ SlotColoring.nativeGap h ∧ ChartScales.nativeIndex h m - commonIndex h n m ≤ SlotColoring.nativeGap h

theorem NavierStokes.CommonCoverClass.adjacent_commonIndex_gap_le (h : ℝ) (hh : 0 ≤ h) {D : ℝ} {L M : SlotColoring.Label} (hadj : SlotColoring.Adj D L M) : ChartScales.nativeIndex h L.1 - commonIndex h L.1 M.1 ≤ SlotColoring.nativeGap h ∧ ChartScales.nativeIndex h M.1 - commonIndex h L.1 M.1 ≤ SlotColoring.nativeGap h

theorem NavierStokes.CommonCoverClass.norm_affine_jet_le_on {X Y V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Y → V} {U : Set Y} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (L : X →L[ℝ] Y) (c : Y) {x : X} (hx : c + L x ∈ U) (j : ℕ) : ‖iteratedFDeriv ℝ j (fun (z : X) => f (c + L z)) x‖ ≤ ‖iteratedFDeriv ℝ j f (c + L x)‖ * ‖L‖ ^ j

theorem NavierStokes.CommonCoverClass.memClass_affine_transport {X Y V : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData Y) (t : WeightedClasses.StripData X) {w : ℕ → Y → ℝ} {v : ℕ → X → ℝ} {α : ℝ} {f : ℕ → Y → V} (hf : WeightedClasses.MemClass s w α f) (index : ℕ → ℕ) (L : ℕ → X →L[ℝ] Y) (c : ℕ → Y) (hmap : ∀ (n : ℕ), ∀ x ∈ t.domain, c n + (L n) x ∈ s.domain) (hweight : ∀ (n : ℕ), ∀ x ∈ t.domain, w (index n) (c n + (L n) x) = v n x) {Ce Cg CL : ℝ} (hCe : 0 ≤ Ce) (hCg : 1 ≤ Cg) (hCL : 1 ≤ CL) (r l : ℕ) (heps : ∀ (n : ℕ), s.epsilon (index n) ^ α ≤ Ce * t.epsilon n ^ α) (hgrowth : ∀ (n : ℕ), ∀ x ∈ t.domain, s.growth (index n) (c n + (L n) x) ≤ Cg * t.growth n x ^ r) (hlinear : ∀ (n : ℕ), ∀ x ∈ t.domain, ‖L n‖ ≤ CL * t.growth n x ^ l) : WeightedClasses.MemClass t v α fun (n : ℕ) (x : X) => f (index n) (c n + (L n) x)

All hypotheses other than the source class concern the actual affine maps and the prescribed weights/scales. No derivative bound on the pulled-back source is a premise. Polynomial map and edge costs do not change the small-scale exponent.

noncomputable def NavierStokes.CommonCoverClass.parameterStrip {X Y : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (s : WeightedClasses.StripData Y) (L : X →L[ℝ] Y) : WeightedClasses.StripData X

A strip over a linear parameter projection. Its weights are the actual base weights, so retaining the parameter preserves them exactly.

Equations

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

@[simp]

theorem NavierStokes.CommonCoverClass.parameterStrip_growth {X Y : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (s : WeightedClasses.StripData Y) (L : X →L[ℝ] Y) (n : ℕ) (x : X) : (parameterStrip s L).growth n x = s.growth n (L x)

noncomputable def NavierStokes.CommonCoverClass.sourceStrip {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) : WeightedClasses.StripData (P × TorusInverse.Plane)

Source strip, given by parameterStrip s (ContinuousLinearMap.fst ℝ P Plane).

Equations

• NavierStokes.CommonCoverClass.sourceStrip s = NavierStokes.CommonCoverClass.parameterStrip s (ContinuousLinearMap.fst ℝ P NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.CommonCoverClass.jointStrip {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (s : WeightedClasses.StripData P) : WeightedClasses.StripData (Joint P)

Joint strip, given by parameterStrip s ((ContinuousLinearMap.fst ℝ P Plane).comp (ContinuousLinearMap.fst ℝ (P × Plane) ℝ)).

Equations

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

theorem NavierStokes.CommonCoverClass.memClass_sourceArgument {P V : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData P) {w : ℕ → P → ℝ} {α : ℝ} {f : ℕ → P × TorusInverse.Plane → V} (hf : WeightedClasses.MemClass (sourceStrip s) (fun (n : ℕ) (z : P × TorusInverse.Plane) => w n z.1) α f) (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h : ℝ} (hh : 0 ≤ h) (D : ℕ) (band gap : ℕ → ℕ) (center : ℕ → TorusInverse.Plane) (copy : ℕ → TorusInverse.Frequency) (hband : ∀ (n : ℕ), 4 ≤ band n) (hgap : ∀ (n : ℕ), gap n ≤ D) (hslow : ∀ (n : ℕ), s.slow n = ChartScales.S (band n)) : WeightedClasses.MemClass (jointStrip s) (fun (n : ℕ) (z : Joint P) => w n z.1.1) α fun (n : ℕ) (z : Joint P) => f n (sourceArgument (bandGeometry B h (band n) (gap n) (center n)) (copy n) z)

Actual all-order class transport along the common-cover path. The indexed band map allows a tail such as band n = n+4. Constants are uniform in all choices of centers and lifted copies.

noncomputable def NavierStokes.CommonCoverClass.coverChange (forward : Bool) (d : ℕ) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

Either direction of a bounded covering change. The inverse is a map on the universal cover; no extra periodicity is imposed on its input.

Equations

• NavierStokes.CommonCoverClass.coverChange forward d = if forward = true then ↑(NavierStokes.CommonCoverSolve.coverPower d) else ↑(NavierStokes.CommonCoverSolve.coverPower d).symm

theorem NavierStokes.CommonCoverClass.norm_coverChange_le (forward : Bool) {d D : ℕ} (hd : d ≤ D) : ‖coverChange forward d‖ ≤ CommonCoverSolve.coveringBound D

noncomputable def NavierStokes.CommonCoverClass.bandCommonChart (D : ℝ) (n m : ℕ) (forward : Bool) (gap : ℕ) : SlowPoint × TorusInverse.Plane →L[ℝ] SlowPoint × TorusInverse.Plane

Band common chart, given by (bandChart D n m).prodMap (coverChange forward gap).

Equations

• NavierStokes.CommonCoverClass.bandCommonChart D n m forward gap = (NavierStokes.CommonCoverClass.bandChart D n m).prodMap (NavierStokes.CommonCoverClass.coverChange forward gap)

@[simp]

theorem NavierStokes.CommonCoverClass.bandCommonChart_apply (D : ℝ) (n m : ℕ) (forward : Bool) (gap : ℕ) (x : SlowPoint × TorusInverse.Plane) : (bandCommonChart D n m forward gap) x = ((bandChart D n m) x.1, (coverChange forward gap) x.2)

noncomputable def NavierStokes.CommonCoverClass.commonChartCost (D : ℝ) (gapBound : ℕ) : ℝ

Common chart cost, given by chartCost D + CommonCoverSolve.coveringBound gapBound.

Equations

• NavierStokes.CommonCoverClass.commonChartCost D gapBound = NavierStokes.CommonCoverClass.chartCost D + NavierStokes.CommonCoverSolve.coveringBound gapBound

theorem NavierStokes.CommonCoverClass.commonChartCost_one_le (D : ℝ) (gapBound : ℕ) : 1 ≤ commonChartCost D gapBound

theorem NavierStokes.CommonCoverClass.norm_bandCommonChart_le (D : ℝ) {n m gap gapBound : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (forward : Bool) (hgap : gap ≤ gapBound) : ‖bandCommonChart D n m forward gap‖ ≤ commonChartCost D gapBound

theorem NavierStokes.CommonCoverClass.bandCommonChart_envelope {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : ℝ) {n m gap gapBound r : ℕ} (hnm : n ≤ m + 4) (hmn : m ≤ n + 4) (forward : Bool) (hgap : gap ≤ gapBound) {f : SlowPoint × TorusInverse.Plane → V} (hf : ContDiff ℝ (↑⊤) f) {e : SlowPoint × TorusInverse.Plane → ℝ} (he : EnvelopeJets r f e) : EnvelopeJets r (fun (x : SlowPoint × TorusInverse.Plane) => f ((bandCommonChart D n m forward gap) x)) fun (x : SlowPoint × TorusInverse.Plane) => e ((bandCommonChart D n m forward gap) x) * commonChartCost D gapBound ^ r

theorem NavierStokes.CommonCoverClass.memClass_bandCommonChart {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (s : WeightedClasses.StripData (SlowPoint × TorusInverse.Plane)) {w v : ℕ → SlowPoint × TorusInverse.Plane → ℝ} {α h : ℝ} {f : ℕ → SlowPoint × TorusInverse.Plane → V} (hf : WeightedClasses.MemClass s w α f) (D : ℝ) (gapBound : ℕ) (band index gap : ℕ → ℕ) (forward : ℕ → Bool) (hband : ∀ (n : ℕ), 1 ≤ band n) (hoverlap : ∀ (n : ℕ), band n ≤ band (index n) + 4 ∧ band (index n) ≤ band n + 4) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) (hepsilon : ∀ (n : ℕ), s.epsilon n = ChartScales.epsilon h (band n)) (hslow : ∀ (n : ℕ), s.slow n = ChartScales.S (band n)) (hmap : ∀ (n : ℕ), ∀ x ∈ s.domain, (bandCommonChart D (band n) (band (index n)) (forward n) (gap n)) x ∈ s.domain) (hdelta : ∀ (n : ℕ), ∀ x ∈ s.domain, s.delta ((bandCommonChart D (band n) (band (index n)) (forward n) (gap n)) x) = s.delta x) (hweight : ∀ (n : ℕ), ∀ x ∈ s.domain, w (index n) ((bandCommonChart D (band n) (band (index n)) (forward n) (gap n)) x) = v n x) : WeightedClasses.MemClass s v α fun (n : ℕ) (x : SlowPoint × TorusInverse.Plane) => f (index n) ((bandCommonChart D (band n) (band (index n)) (forward n) (gap n)) x)

Class transport under the actual simultaneous slow-chart and bounded covering change. The weight/edge identities express the same physical profile in the two charts; they are geometric identities, not jet bounds.

theorem NavierStokes.CommonCoverClass.bandChart_eq_transition (h : ℝ) (n m : ℕ) (x : SlowPoint) : (bandChart (CoordinateAlgebra.D h) n m) x = SimilarityHomogeneity.chartTransition h (ChartScales.Q n) (ChartScales.Q m) x

theorem NavierStokes.CommonCoverClass.profileX_bandChart {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n m : ℕ) {x : SlowPoint} (hx : 0 < x.2.2) : SimilarityHomogeneity.chartX h ((bandChart (CoordinateAlgebra.D h) n m) x) = SimilarityHomogeneity.chartX h x

theorem NavierStokes.CommonCoverClass.profileEta_bandChart {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n m : ℕ) {x : SlowPoint} (hx : 0 < x.2.2) : SimilarityHomogeneity.chartEta h ((bandChart (CoordinateAlgebra.D h) n m) x) = SimilarityHomogeneity.chartEta h x

noncomputable def NavierStokes.CommonCoverClass.profileDomain (h a b : ℝ) : Set SlowPoint

Profile domain, given by {x | x ∈ SimilarityHomogeneity.chartDomain ∧ SimilarityHomogeneity.chartX h x ∈ Ioo a b}.

Equations

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

theorem NavierStokes.CommonCoverClass.profileX_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : SlowPoint} (hx : 0 < x.2.2) : ContDiffAt ℝ (↑⊤) (SimilarityHomogeneity.chartX h) x

theorem NavierStokes.CommonCoverClass.isOpen_profileDomain {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (a b : ℝ) : IsOpen (profileDomain h a b)

theorem NavierStokes.CommonCoverClass.profileDomain_bandChart {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n m : ℕ) {x : SlowPoint} (hx : x ∈ profileDomain h a b) : (bandChart (CoordinateAlgebra.D h) n m) x ∈ profileDomain h a b

noncomputable def NavierStokes.CommonCoverClass.profileSlowStrip {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (band : ℕ → ℕ) (hband : ∀ (n : ℕ), 1 ≤ band n) (ζ : ℝ → ℝ) (hζ : ContDiff ℝ (↑⊤) ζ) (hζ0 : ∀ X ∈ Set.Ioo a b, 0 ≤ ζ X) : WeightedClasses.StripData SlowPoint

A concrete strip with the physical profile weight and logarithmic distance. The independent index chooses the actual dyadic band.

Equations

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

theorem NavierStokes.CommonCoverClass.memClass_profile_bandCommonChart {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (band : ℕ → ℕ) (hband : ∀ (n : ℕ), 1 ≤ band n) (ζ : ℝ → ℝ) (hζ : ContDiff ℝ (↑⊤) ζ) (hζ0 : ∀ X ∈ Set.Ioo a b, 0 ≤ ζ X) {w v : ℕ → SlowPoint × TorusInverse.Plane → ℝ} {α : ℝ} {f : ℕ → SlowPoint × TorusInverse.Plane → V} (hf : WeightedClasses.MemClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) w α f) (gapBound : ℕ) (index gap : ℕ → ℕ) (forward : ℕ → Bool) (hoverlap : ∀ (n : ℕ), band n ≤ band (index n) + 4 ∧ band (index n) ≤ band n + 4) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) (hweight : ∀ (n : ℕ) (x : SlowPoint × TorusInverse.Plane), x.1 ∈ profileDomain h a b → w (index n) ((bandCommonChart (CoordinateAlgebra.D h) (band n) (band (index n)) (forward n) (gap n)) x) = v n x) : WeightedClasses.MemClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) v α fun (n : ℕ) (x : SlowPoint × TorusInverse.Plane) => f (index n) ((bandCommonChart (CoordinateAlgebra.D h) (band n) (band (index n)) (forward n) (gap n)) x)

Here the domain and the edge identity are proved from actual profile homogeneity. Only the prescribed additional weight is transported.

theorem NavierStokes.CommonCoverClass.meanClass_profile_bandCommonChart {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (band : ℕ → ℕ) (hband : ∀ (n : ℕ), 1 ≤ band n) (ζ : ℝ → ℝ) (hζ : ContDiff ℝ (↑⊤) ζ) (hζ0 : ∀ X ∈ Set.Ioo a b, 0 ≤ ζ X) {α : ℝ} {f : ℕ → SlowPoint × TorusInverse.Plane → V} (hf : WeightedClasses.MeanClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) α f) (gapBound : ℕ) (index gap : ℕ → ℕ) (forward : ℕ → Bool) (hoverlap : ∀ (n : ℕ), band n ≤ band (index n) + 4 ∧ band (index n) ≤ band n + 4) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) : WeightedClasses.MeanClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) α fun (n : ℕ) (x : SlowPoint × TorusInverse.Plane) => f (index n) ((bandCommonChart (CoordinateAlgebra.D h) (band n) (band (index n)) (forward n) (gap n)) x)

The actual mean class is preserved, with exactly the same small-scale exponent, under all overlapping band/common-cover changes.

theorem NavierStokes.CommonCoverClass.waveClass_profile_bandCommonChart {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {h a b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (band : ℕ → ℕ) (hband : ∀ (n : ℕ), 1 ≤ band n) (ζ : ℝ → ℝ) (hζ : ContDiff ℝ (↑⊤) ζ) (hζ0 : ∀ X ∈ Set.Ioo a b, 0 ≤ ζ X) (P : ℕ → SlowPoint × TorusInverse.Plane → ℝ) {α : ℝ} {f : ℕ → SlowPoint × TorusInverse.Plane → V} (hf : WeightedClasses.WaveClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) P α f) (gapBound : ℕ) (index gap : ℕ → ℕ) (forward : ℕ → Bool) (hoverlap : ∀ (n : ℕ), band n ≤ band (index n) + 4 ∧ band (index n) ≤ band n + 4) (hgap : ∀ (n : ℕ), gap n ≤ gapBound) : WeightedClasses.WaveClass (sourceStrip (profileSlowStrip hh hh1 ha band hband ζ hζ hζ0)) (fun (n : ℕ) (x : SlowPoint × TorusInverse.Plane) => P (index n) ((bandCommonChart (CoordinateAlgebra.D h) (band n) (band (index n)) (forward n) (gap n)) x)) α fun (n : ℕ) (x : SlowPoint × TorusInverse.Plane) => f (index n) ((bandCommonChart (CoordinateAlgebra.D h) (band n) (band (index n)) (forward n) (gap n)) x)

The wave envelope is transported at its actual point. The radial factor and edge distance are invariant; the slot profile is pulled back exactly and is not replaced by another label's profile.

noncomputable def NavierStokes.CommonCoverClass.meshCoordinate (D : ℝ) (L : SlotColoring.Label) (x : SlotColoring.Position) : SlotColoring.Position

Normalized small slow-box coordinates, using the actual widths from the coloring construction.

Equations

• NavierStokes.CommonCoverClass.meshCoordinate D L x j = (x j - NavierStokes.SlotColoring.width D j L.1 * ↑(L.2.1 j)) / NavierStokes.SlotColoring.width D j L.1

noncomputable def NavierStokes.CommonCoverClass.meshPoint (D : ℝ) (L : SlotColoring.Label) (x : SlotColoring.Position) : SlotColoring.Position

Mesh point, defined pointwise by SlotColoring.width D j L.1 * x j + SlotColoring.width D j L.1 * (L.2.1 j : ℝ).

Equations

• NavierStokes.CommonCoverClass.meshPoint D L x j = NavierStokes.SlotColoring.width D j L.1 * x j + NavierStokes.SlotColoring.width D j L.1 * ↑(L.2.1 j)

noncomputable def NavierStokes.CommonCoverClass.meshLinear (D : ℝ) (L M : SlotColoring.Label) : SlotColoring.Position →L[ℝ] SlotColoring.Position

Mesh linear, constructed using ContinuousLinearMap.pi.

Equations

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

noncomputable def NavierStokes.CommonCoverClass.meshOffset (D : ℝ) (L M : SlotColoring.Label) : SlotColoring.Position

Mesh offset, defined pointwise by (SlotColoring.width D j L.1 * (L.2.1 j : ℝ) - SlotColoring.width D j M.1 * (M.2.1 j : ℝ)) / SlotColoring.width D j M.1.

Equations

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

noncomputable def NavierStokes.CommonCoverClass.meshTransition (D : ℝ) (L M : SlotColoring.Label) (x : SlotColoring.Position) : SlotColoring.Position

Mesh transition, given by meshOffset D L M + meshLinear D L M x.

Equations

• NavierStokes.CommonCoverClass.meshTransition D L M x = NavierStokes.CommonCoverClass.meshOffset D L M + (NavierStokes.CommonCoverClass.meshLinear D L M) x

@[simp]

theorem NavierStokes.CommonCoverClass.meshLinear_apply (D : ℝ) (L M : SlotColoring.Label) (x : SlotColoring.Position) (j : Fin 3) : (meshLinear D L M) x j = SlotColoring.width D j L.1 / SlotColoring.width D j M.1 * x j

theorem NavierStokes.CommonCoverClass.meshTransition_eq_coordinate (D : ℝ) (L M : SlotColoring.Label) (x : SlotColoring.Position) : meshTransition D L M x = meshCoordinate D M (meshPoint D L x)

theorem NavierStokes.CommonCoverClass.mesh_ratioBound_pos (D : ℝ) : 0 < SlotColoring.ratioBound D

theorem NavierStokes.CommonCoverClass.norm_meshLinear_le {D : ℝ} {L M : SlotColoring.Label} (h : SlotColoring.Adj D L M) : ‖meshLinear D L M‖ ≤ SlotColoring.ratioBound D

Only physical-box adjacency is assumed; the normalized coordinate change is bounded uniformly over all box indices and levels.

theorem NavierStokes.CommonCoverClass.norm_meshOffset_le {D : ℝ} {L M : SlotColoring.Label} (h : SlotColoring.Adj D L M) : ‖meshOffset D L M‖ ≤ 2 * (SlotColoring.ratioBound D + 1)

The translation is controlled by genuine support overlap. It is not bounded by assuming the lattice copy indices themselves are bounded.

theorem NavierStokes.CommonCoverClass.meshTransition_smooth (D : ℝ) (L M : SlotColoring.Label) : ContDiff ℝ (↑⊤) (meshTransition D L M)

theorem NavierStokes.CommonCoverClass.meshTransition_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {D : ℝ} {L M : SlotColoring.Label} (h : SlotColoring.Adj D L M) {f : SlotColoring.Position → V} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (x : SlotColoring.Position) {A : ℝ} (hb : ∀ j ≤ m, ‖iteratedFDeriv ℝ j f (meshTransition D L M x)‖ ≤ A) (j : ℕ) : j ≤ m → ‖iteratedFDeriv ℝ j (fun (y : SlotColoring.Position) => f (meshTransition D L M y)) x‖ ≤ A * (1 + SlotColoring.ratioBound D) ^ m

theorem NavierStokes.CommonCoverClass.meshTransition_norm_le {D : ℝ} {L M : SlotColoring.Label} (h : SlotColoring.Adj D L M) {x : SlotColoring.Position} (hx : ‖x‖ ≤ 2) : ‖meshTransition D L M x‖ ≤ 4 * SlotColoring.ratioBound D + 2

theorem NavierStokes.CommonCoverClass.adjacent_argumentCost_le (B : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane) {h D : ℝ} (hh : 0 ≤ h) {L M : SlotColoring.Label} (hadj : SlotColoring.Adj D L M) (hL : 4 ≤ L.1) (center : TorusInverse.Plane) : argumentCost (bandGeometry B h L.1 (ChartScales.nativeIndex h L.1 - commonIndex h L.1 M.1) center) ≤ bandArgumentCost B (SlotColoring.nativeGap h) * ChartScales.S L.1

The covering budget used in the path estimate is now instantiated from the actual adjacent labels and their coarsest common native index.

noncomputable def NavierStokes.CommonCoverClass.nativeBasis : TorusInverse.Plane ≃L[ℝ] TorusInverse.Plane

The actual radial/time eigenvector basis, not an abstract invertible basis supplied as an assumption.

Equations

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

theorem NavierStokes.CommonCoverClass.nativeBasis_radial : nativeBasis (1, 0) = PhysicalGraphBounds.radialDirection

theorem NavierStokes.CommonCoverClass.nativeBasis_temporal : nativeBasis (0, 1) = PhysicalGraphBounds.timeDirection

theorem NavierStokes.CommonCoverClass.native_band_path (h : ℝ) (n gap : ℕ) (center : TorusInverse.Plane) (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : CommonCoverSolve.Geometry.path (bandGeometry nativeBasis h n gap center) k Y s = Y + (CommonCoverSolve.coverPower gap).symm ((ChartScales.timeCoefficient h n * (s - (CommonCoverSolve.Geometry.coordinates (bandGeometry nativeBasis h n gap center) k Y).2)) • PhysicalGraphBounds.timeDirection)

The exact manuscript path, with the actual c_i and v_t.

theorem NavierStokes.CommonCoverClass.exists_coarsest_band (h : ℝ) (hh : 0 ≤ h) (levels : Finset ℕ) (hne : levels.Nonempty) (hpos : ∀ n ∈ levels, 1 ≤ n) (hspan : ∀ n ∈ levels, ∀ m ∈ levels, n ≤ m + 4) : ∃ c ∈ levels, ∀ n ∈ levels, ChartScales.nativeIndex h c ≤ ChartScales.nativeIndex h n ∧ ChartScales.nativeIndex h n - ChartScales.nativeIndex h c ≤ SlotColoring.nativeGap h

Any finite collection of active levels with the geometric level-span bound has a genuine coarsest member and a uniform covering budget to it.