Compatibility of the actual copy-path solve with a common-cover change

The native slot is held fixed while the common cover is refined. Sources are pulled back along the covering map. Equality is proved first for the actual coefficient/forcing paths and then for the constructed Volterra inverse; no native periodicity of an inhomogeneous solution is assumed.

theorem NavierStokes.CopySolveCompatibility.coverPower_add (d k : ℕ) (Y : TorusInverse.Plane) : (CommonCoverSolve.coverPower (d + k)) Y = (CommonCoverSolve.coverPower d) ((CommonCoverSolve.coverPower k) Y)

noncomputable def NavierStokes.CopySolveCompatibility.refineGeometry (g : CommonCoverSolve.Geometry) (k : ℕ) : CommonCoverSolve.Geometry

Refine geometry, given by { g with gap := g.gap + k }.

Equations

• NavierStokes.CopySolveCompatibility.refineGeometry g k = { gap := g.gap + k, basis := g.basis, center := g.center }

theorem NavierStokes.CopySolveCompatibility.coordinates_refine (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (refineGeometry g k).coordinates j Y = g.coordinates j ((CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.point_refine (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (z : TorusInverse.Plane) : (CommonCoverSolve.coverPower k) ((refineGeometry g k).point j z) = g.point j z

theorem NavierStokes.CopySolveCompatibility.path_refine (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : (CommonCoverSolve.coverPower k) ((refineGeometry g k).path j Y s) = g.path j ((CommonCoverSolve.coverPower k) Y) s

theorem NavierStokes.CopySolveCompatibility.cutoff_refine (g : CommonCoverSolve.Geometry) (k : ℕ) (κ : TorusInverse.Plane → ℝ) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) : κ ((refineGeometry g k).coordinates j Y) = κ (g.coordinates j ((CommonCoverSolve.coverPower k) Y))

theorem NavierStokes.CopySolveCompatibility.native_copy_sum_refine {E : Type} [NormedAddCommGroup E] (g : CommonCoverSolve.Geometry) (k : ℕ) (f : TorusInverse.Plane → E) (Y : TorusInverse.Plane) : ∑' (j : TorusInverse.Frequency), f ((refineGeometry g k).coordinates j Y) = ∑' (j : TorusInverse.Frequency), f (g.coordinates j ((CommonCoverSolve.coverPower k) Y))

This includes cutoff indicators and copy envelopes, with no regularity assumption on the native function.

noncomputable def NavierStokes.CopySolveCompatibility.transformData {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (k : ℕ) : CommonCoverSolve.LinearData Q V E

Input data transported through a slow-parameter map and a refinement of the common cover. All native coefficients retain their native arguments.

Equations

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

noncomputable def NavierStokes.CopySolveCompatibility.pullbackData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (k : ℕ) : CommonCoverSolve.LinearData P V E

Pullback data, given by transformData d id k.

Equations

• NavierStokes.CopySolveCompatibility.pullbackData d k = NavierStokes.CopySolveCompatibility.transformData d id k

theorem NavierStokes.CopySolveCompatibility.coefficientAlong_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) (s : ℝ) : (transformData d φ k).coefficientAlong (refineGeometry g k) j ((q, Y), s) = d.coefficientAlong g j ((φ q, (CommonCoverSolve.coverPower k) Y), s)

theorem NavierStokes.CopySolveCompatibility.forcingAlong_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) (s : ℝ) : (transformData d φ k).forcingAlong (refineGeometry g k) j ((q, Y), s) = d.forcingAlong g j ((φ q, (CommonCoverSolve.coverPower k) Y), s)

theorem NavierStokes.CopySolveCompatibility.pathFamily_congr {P Q E : Type} [NormedAddCommGroup E] {a b : ℝ} (F : P × ℝ → E) (G : Q × ℝ → E) (p : P) (q : Q) (h : ∀ (s : ↑(Set.Icc a b)), F (p, ↑s) = G (q, ↑s)) : SmoothPathFamily.pathFamily F p = SmoothPathFamily.pathFamily G q

Equality of input paths may compare different parameter spaces. The canonical zero branch for a noncontinuous slice is respected as well.

theorem NavierStokes.CopySolveCompatibility.coefficientPath_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : (transformData d φ k).coefficientPath (refineGeometry g k) j (q, Y) = d.coefficientPath g j (φ q, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.forcingPath_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : (transformData d φ k).forcingPath (refineGeometry g k) j (q, Y) = d.forcingPath g j (φ q, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.anchoredSolve_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) (s : ℝ) : (transformData d φ k).anchoredSolve (refineGeometry g k) hab j (q, Y) s = d.anchoredSolve g hab j (φ q, (CommonCoverSolve.coverPower k) Y) s

theorem NavierStokes.CopySolveCompatibility.copySolve_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : (transformData d φ k).copySolve (refineGeometry g k) hab j (q, Y) = d.copySolve g hab j (φ q, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.localizedCopy_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (κ : TorusInverse.Plane → ℝ) (j : TorusInverse.Frequency) (q : Q) (Y : TorusInverse.Plane) : (transformData d φ k).localizedCopy (refineGeometry g k) hab κ j (q, Y) = d.localizedCopy g hab κ j (φ q, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.commonSolve_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (κ : TorusInverse.Plane → ℝ) (q : Q) (Y : TorusInverse.Plane) : (transformData d φ k).commonSolve (refineGeometry g k) hab κ (q, Y) = d.commonSolve g hab κ (φ q, (CommonCoverSolve.coverPower k) Y)

Equality of the actual periodized solves, obtained term by term before forming the sum. No periodicity hypothesis on a native inhomogeneous solve is used, or needed.

theorem NavierStokes.CopySolveCompatibility.commonSolve_refine {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (κ : TorusInverse.Plane → ℝ) (p : P) (Y : TorusInverse.Plane) : (pullbackData d k).commonSolve (refineGeometry g k) hab κ (p, Y) = d.commonSolve g hab κ (p, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.source_periodic_transform {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (k : ℕ) (q : Q) (hp : CommonCoverSolve.PeriodicAt d.source (φ q)) : CommonCoverSolve.PeriodicAt (transformData d φ k).source q

theorem NavierStokes.CopySolveCompatibility.commonOnTorus_refine {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (κ : TorusInverse.Plane → ℝ) (p : P) (hp : CommonCoverSolve.PeriodicAt d.source p) (Y : TorusInverse.Plane) : (pullbackData d k).commonOnTorus (refineGeometry g k) hab κ p ⋯ (TorusAverages.quotientPoint Y) = d.commonOnTorus g hab κ p hp (TorusAverages.quotientPoint ((CommonCoverSolve.coverPower k) Y))

Changing the integer representative of the native slot center

noncomputable def NavierStokes.CopySolveCompatibility.recenterGeometry (g : CommonCoverSolve.Geometry) (l : TorusInverse.Frequency) : CommonCoverSolve.Geometry

Recenter geometry, given by { g with center := g.center + TorusAverages.latticePoint l }.

Equations

• NavierStokes.CopySolveCompatibility.recenterGeometry g l = { gap := g.gap, basis := g.basis, center := g.center + NavierStokes.TorusAverages.latticePoint l }

theorem NavierStokes.CopySolveCompatibility.coordinates_recenter (g : CommonCoverSolve.Geometry) (l j : TorusInverse.Frequency) (Y : TorusInverse.Plane) : (recenterGeometry g l).coordinates j Y = g.coordinates (j + l) Y

theorem NavierStokes.CopySolveCompatibility.point_recenter (g : CommonCoverSolve.Geometry) (l j : TorusInverse.Frequency) (z : TorusInverse.Plane) : (recenterGeometry g l).point j z = g.point (j + l) z

theorem NavierStokes.CopySolveCompatibility.path_recenter (g : CommonCoverSolve.Geometry) (l j : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : (recenterGeometry g l).path j Y s = g.path (j + l) Y s

theorem NavierStokes.CopySolveCompatibility.anchoredSolve_recenter {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (l j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : d.anchoredSolve (recenterGeometry g l) hab j (p, Y) s = d.anchoredSolve g hab (j + l) (p, Y) s

theorem NavierStokes.CopySolveCompatibility.copySolve_recenter {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (l j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) : d.copySolve (recenterGeometry g l) hab j (p, Y) = d.copySolve g hab (j + l) (p, Y)

theorem NavierStokes.CopySolveCompatibility.localizedCopy_recenter {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (l j : TorusInverse.Frequency) (κ : TorusInverse.Plane → ℝ) (p : P) (Y : TorusInverse.Plane) : d.localizedCopy (recenterGeometry g l) hab κ j (p, Y) = d.localizedCopy g hab κ (j + l) (p, Y)

theorem NavierStokes.CopySolveCompatibility.commonSolve_recenter {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (l : TorusInverse.Frequency) (κ : TorusInverse.Plane → ℝ) (p : P) (Y : TorusInverse.Plane) : d.commonSolve (recenterGeometry g l) hab κ (p, Y) = d.commonSolve g hab κ (p, Y)

Physical units: scaling the actual source scales the actual solution

noncomputable def NavierStokes.CopySolveCompatibility.scaleSource {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (c : ℝ) : CommonCoverSolve.LinearData P V E

Scale source, given by { d with source := fun x => c • d.source x }.

Equations

• NavierStokes.CopySolveCompatibility.scaleSource d c = { coefficient := d.coefficient, forcingMap := d.forcingMap, source := fun (x : P × NavierStokes.TorusInverse.Plane) => c • d.source x }

theorem NavierStokes.CopySolveCompatibility.pathFamily_smul {P E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (F : P × ℝ → E) (p : P) (c : ℝ) : SmoothPathFamily.pathFamily (fun (x : P × ℝ) => c • F x) p = c • SmoothPathFamily.pathFamily F p

theorem NavierStokes.CopySolveCompatibility.solution_zero_smul {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : ParametricODE.Coefficient a b E) (f : ParametricODE.Curve a b E) (c : ℝ) : ParametricODE.solution hab A 0 (c • f) = c • ParametricODE.solution hab A 0 f

theorem NavierStokes.CopySolveCompatibility.solutionExtension_zero_smul {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : ParametricODE.Coefficient a b E) (f : ParametricODE.Curve a b E) (c s : ℝ) : ParametricODE.solutionExtension hab A 0 (c • f) s = c • ParametricODE.solutionExtension hab A 0 f s

theorem NavierStokes.CopySolveCompatibility.anchoredSolve_scaleSource {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (c : ℝ) (j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : (scaleSource d c).anchoredSolve g hab j (p, Y) s = c • d.anchoredSolve g hab j (p, Y) s

theorem NavierStokes.CopySolveCompatibility.copySolve_scaleSource {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (c : ℝ) (j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) : (scaleSource d c).copySolve g hab j (p, Y) = c • d.copySolve g hab j (p, Y)

theorem NavierStokes.CopySolveCompatibility.localizedCopy_scaleSource {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (c : ℝ) (κ : TorusInverse.Plane → ℝ) (j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) : (scaleSource d c).localizedCopy g hab κ j (p, Y) = c • d.localizedCopy g hab κ j (p, Y)

theorem NavierStokes.CopySolveCompatibility.commonSolve_scaleSource {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (c : ℝ) (κ : TorusInverse.Plane → ℝ) (p : P) (Y : TorusInverse.Plane) : (scaleSource d c).commonSolve g hab κ (p, Y) = c • d.commonSolve g hab κ (p, Y)

Transporting the native clock, its anchor, and its cutoff together

noncomputable def NavierStokes.CopySolveCompatibility.nativeTimeMap (τ rate : ℝ) (z : TorusInverse.Plane) : TorusInverse.Plane

Native time map, given by (z.1, τ + rate * z.2).

Equations

• NavierStokes.CopySolveCompatibility.nativeTimeMap τ rate z = (z.1, τ + rate * z.2)

theorem NavierStokes.CopySolveCompatibility.nativeTimeMap_continuous (τ rate : ℝ) : Continuous (nativeTimeMap τ rate)

noncomputable def NavierStokes.CopySolveCompatibility.timeGeometry (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) : CommonCoverSolve.Geometry

Time geometry, bundling gap, basis, center.

Equations

• NavierStokes.CopySolveCompatibility.timeGeometry g τ rate hrate = { gap := g.gap, basis := NavierStokes.CommonCoverClass.scaledBasis g.basis rate hrate, center := g.center + g.basis (0, τ) }

theorem NavierStokes.CopySolveCompatibility.point_timeGeometry (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (z : TorusInverse.Plane) : (timeGeometry g τ rate hrate).point j z = g.point j (nativeTimeMap τ rate z)

theorem NavierStokes.CopySolveCompatibility.coordinates_timeGeometry (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) : nativeTimeMap τ rate ((timeGeometry g τ rate hrate).coordinates j Y) = g.coordinates j Y

theorem NavierStokes.CopySolveCompatibility.coordinates_timeGeometry_fst (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) : ((timeGeometry g τ rate hrate).coordinates j Y).1 = (g.coordinates j Y).1

theorem NavierStokes.CopySolveCompatibility.path_timeGeometry (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : (timeGeometry g τ rate hrate).path j Y s = g.path j Y (τ + rate * s)

theorem NavierStokes.CopySolveCompatibility.time_interval_mono {a b rate : ℝ} (τ : ℝ) (hrate : 0 < rate) (hab : a ≤ b) : τ + rate * a ≤ τ + rate * b

noncomputable def NavierStokes.CopySolveCompatibility.timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (τ rate : ℝ) : CommonCoverSolve.LinearData P V E

Time data, bundling coefficient, forcingMap, source.

Equations

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

theorem NavierStokes.CopySolveCompatibility.coefficientAlong_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : (timeData d τ rate).coefficientAlong (timeGeometry g τ rate hrate) j ((p, Y), s) = rate • d.coefficientAlong g j ((p, Y), τ + rate * s)

theorem NavierStokes.CopySolveCompatibility.forcingAlong_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : rate ≠ 0) (j : TorusInverse.Frequency) (p : P) (Y : TorusInverse.Plane) (s : ℝ) : (timeData d τ rate).forcingAlong (timeGeometry g τ rate hrate) j ((p, Y), s) = rate • d.forcingAlong g j ((p, Y), τ + rate * s)

theorem NavierStokes.CopySolveCompatibility.timeData_coefficient_continuousOn {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] (d : CommonCoverSolve.LinearData P V E) (τ rate : ℝ) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) : ContinuousOn (timeData d τ rate).coefficient (U ×ˢ Set.univ)

theorem NavierStokes.CopySolveCompatibility.timeData_forcingMap_continuousOn {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] (d : CommonCoverSolve.LinearData P V E) (τ rate : ℝ) {U : Set P} (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) : ContinuousOn (timeData d τ rate).forcingMap (U ×ˢ Set.univ)

theorem NavierStokes.CopySolveCompatibility.anchoredSolve_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : 0 < rate) (hab : a ≤ b) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (j : TorusInverse.Frequency) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) {s : ℝ} (hs : s ∈ Set.Icc a b) : (timeData d τ rate).anchoredSolve (timeGeometry g τ rate ⋯) hab j (p, Y) s = d.anchoredSolve g ⋯ j (p, Y) (τ + rate * s)

Clock transport is proved from uniqueness of the actual zero-entry Volterra solution on the transported interval.

theorem NavierStokes.CopySolveCompatibility.copySolve_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : 0 < rate) (hab : a ≤ b) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (j : TorusInverse.Frequency) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) (hs : ((timeGeometry g τ rate ⋯).coordinates j Y).2 ∈ Set.Icc a b) : (timeData d τ rate).copySolve (timeGeometry g τ rate ⋯) hab j (p, Y) = d.copySolve g ⋯ j (p, Y)

theorem NavierStokes.CopySolveCompatibility.localizedCopy_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : 0 < rate) (hab : a ≤ b) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc (τ + rate * a) (τ + rate * b)) (j : TorusInverse.Frequency) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) : (timeData d τ rate).localizedCopy (timeGeometry g τ rate ⋯) hab (κ ∘ nativeTimeMap τ rate) j (p, Y) = d.localizedCopy g ⋯ κ j (p, Y)

theorem NavierStokes.CopySolveCompatibility.commonSolve_timeData {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (τ rate : ℝ) (hrate : 0 < rate) (hab : a ≤ b) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc (τ + rate * a) (τ + rate * b)) {p : P} (hp : p ∈ U) (Y : TorusInverse.Plane) : (timeData d τ rate).commonSolve (timeGeometry g τ rate ⋯) hab (κ ∘ nativeTimeMap τ rate) (p, Y) = d.commonSolve g ⋯ κ (p, Y)

A single output represented in all transported charts

noncomputable def NavierStokes.CopySolveCompatibility.transportData {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (k : ℕ) (τ rate amplitude : ℝ) : CommonCoverSolve.LinearData Q V E

Transport data, given by scaleSource (transformData (timeData d τ rate) φ k) amplitude.

Equations

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

noncomputable def NavierStokes.CopySolveCompatibility.transportGeometry (g : CommonCoverSolve.Geometry) (k : ℕ) (τ rate : ℝ) (hrate : rate ≠ 0) : CommonCoverSolve.Geometry

Transport geometry, given by refineGeometry (timeGeometry g τ rate hrate) k.

Equations

• NavierStokes.CopySolveCompatibility.transportGeometry g k τ rate hrate = NavierStokes.CopySolveCompatibility.refineGeometry (NavierStokes.CopySolveCompatibility.timeGeometry g τ rate hrate) k

theorem NavierStokes.CopySolveCompatibility.commonSolve_transport {P Q V E : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (τ rate amplitude : ℝ) (hrate : 0 < rate) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc (τ + rate * a) (τ + rate * b)) (q : Q) (hq : φ q ∈ U) (Y : TorusInverse.Plane) : (transportData d φ k τ rate amplitude).commonSolve (transportGeometry g k τ rate ⋯) hab (κ ∘ nativeTimeMap τ rate) (q, Y) = amplitude • d.commonSolve g ⋯ κ (φ q, (CommonCoverSolve.coverPower k) Y)

noncomputable def NavierStokes.CopySolveCompatibility.physicalOutput {P V E X : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (κ : TorusInverse.Plane → ℝ) (χ : X → P × TorusInverse.Plane) : X → E

Physical output, defined pointwise by d.commonSolve g hab κ (χ x).

Equations

• NavierStokes.CopySolveCompatibility.physicalOutput d g hab κ χ x = d.commonSolve g hab κ (χ x)

theorem NavierStokes.CopySolveCompatibility.physicalOutput_contDiffOn {P V E X : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup X] [NormedSpace ℝ X] {a b : ℝ} (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) {U : Set P} (hU : IsOpen U) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (U ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (U ×ˢ Set.univ)) {κ : TorusInverse.Plane → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsupp : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo a b) {Ω : Set X} {χ : X → P × TorusInverse.Plane} (hχ : ContDiffOn ℝ (↑⊤) χ Ω) (hmaps : Set.MapsTo χ Ω (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (physicalOutput d g hab κ χ) Ω

The single reference output is an actual smooth field under the usual compact native cutoff and smooth input hypotheses. Local finiteness of the periodization is supplied by the constructed copy solver.

theorem NavierStokes.CopySolveCompatibility.commonSolve_family_represents {P Q V E X I : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {A B : ℝ} (hAB : A ≤ B) (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc A B) (χ : X → P × TorusInverse.Plane) (domains : I → Set X) (charts : I → X → Q × TorusInverse.Plane) (φ : I → Q → P) (gaps : I → ℕ) (entry exit shift rate amplitude : I → ℝ) (hrate : ∀ (i : I), 0 < rate i) (hinterval : ∀ (i : I), entry i ≤ exit i) (hentry : ∀ (i : I), shift i + rate i * entry i = A) (hexit : ∀ (i : I), shift i + rate i * exit i = B) (hchart : ∀ (i : I), ∀ x ∈ domains i, (φ i (charts i x).1, (CommonCoverSolve.coverPower (gaps i)) (charts i x).2) = χ x) (hslow : ∀ (i : I), ∀ x ∈ domains i, (χ x).1 ∈ U) (i : I) (x : X) : x ∈ domains i → (transportData d (φ i) (gaps i) (shift i) (rate i) (amplitude i)).commonSolve (transportGeometry g (gaps i) (shift i) (rate i) ⋯) ⋯ (κ ∘ nativeTimeMap (shift i) (rate i)) (charts i x) = amplitude i • physicalOutput d g hAB κ χ x

The family of chart solves represents one explicitly constructed physical field. Assumptions concern only input transport and the coordinate maps; no output equality or chartwise existence witness is assumed.

theorem NavierStokes.CopySolveCompatibility.commonSolve_bandCommonChart {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d : CommonCoverSolve.LinearData CommonCoverClass.SlowPoint V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (D : ℝ) (n m k : ℕ) (κ : TorusInverse.Plane → ℝ) (x : CommonCoverClass.SlowPoint × TorusInverse.Plane) : (transformData d (⇑(CommonCoverClass.bandChart D n m)) k).commonSolve (refineGeometry g k) hab κ x = d.commonSolve g hab κ ((CommonCoverClass.bandCommonChart D n m true k) x)

The slow/torus argument is exactly the existing common-band chart map.

Binding existing chart data through primitive input identities

structure NavierStokes.CopySolveCompatibility.SameInputsAt {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (d e : CommonCoverSolve.LinearData P V E) (p : P) : Prop

These are identities of the coefficient and converted source before any integration. They allow different source/map scalings with the same product, and impose no assertion about solved fields.

• coefficient (z : TorusInverse.Plane) : d.coefficient (p, z) = e.coefficient (p, z)
• forcing (z Y : TorusInverse.Plane) : (d.forcingMap (p, z)) (d.source (p, Y)) = (e.forcingMap (p, z)) (e.source (p, Y))

theorem NavierStokes.CopySolveCompatibility.anchoredSolve_eq_of_sameInputs {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d e : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (p : P) (hi : SameInputsAt d e p) (j : TorusInverse.Frequency) (Y : TorusInverse.Plane) (s : ℝ) : d.anchoredSolve g hab j (p, Y) s = e.anchoredSolve g hab j (p, Y) s

theorem NavierStokes.CopySolveCompatibility.commonSolve_eq_of_sameInputs {P V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (d e : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (p : P) (hi : SameInputsAt d e p) (κ : TorusInverse.Plane → ℝ) (Y : TorusInverse.Plane) : d.commonSolve g hab κ (p, Y) = e.commonSolve g hab κ (p, Y)

theorem NavierStokes.CopySolveCompatibility.commonSolve_of_compatibleInputs {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : CommonCoverSolve.LinearData P V E) (e : CommonCoverSolve.LinearData Q V E) (φ : Q → P) (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (k : ℕ) (τ rate amplitude : ℝ) (hrate : 0 < rate) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc (τ + rate * a) (τ + rate * b)) (q : Q) (hq : φ q ∈ U) (hi : SameInputsAt e (transportData d φ k τ rate amplitude) q) (Y : TorusInverse.Plane) : e.commonSolve (transportGeometry g k τ rate ⋯) hab (κ ∘ nativeTimeMap τ rate) (q, Y) = amplitude • d.commonSolve g ⋯ κ (φ q, (CommonCoverSolve.coverPower k) Y)

theorem NavierStokes.CopySolveCompatibility.compatible_family_represents {P Q V E X I : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup P] [NormedSpace ℝ P] {A B : ℝ} (hAB : A ≤ B) (d : CommonCoverSolve.LinearData P V E) (g : CommonCoverSolve.Geometry) {U : Set P} (hA : ContinuousOn d.coefficient (U ×ˢ Set.univ)) (hB : ContinuousOn d.forcingMap (U ×ˢ Set.univ)) (hf : ContinuousOn d.source (U ×ˢ Set.univ)) (κ : TorusInverse.Plane → ℝ) (hκ : Function.support κ ⊆ Set.univ ×ˢ Set.Icc A B) (χ : X → P × TorusInverse.Plane) (domains : I → Set X) (charts : I → X → Q × TorusInverse.Plane) (φ : I → Q → P) (gaps : I → ℕ) (entry exit shift rate amplitude : I → ℝ) (hrate : ∀ (i : I), 0 < rate i) (hinterval : ∀ (i : I), entry i ≤ exit i) (hentry : ∀ (i : I), shift i + rate i * entry i = A) (hexit : ∀ (i : I), shift i + rate i * exit i = B) (hchart : ∀ (i : I), ∀ x ∈ domains i, (φ i (charts i x).1, (CommonCoverSolve.coverPower (gaps i)) (charts i x).2) = χ x) (hslow : ∀ (i : I), ∀ x ∈ domains i, (χ x).1 ∈ U) (data : I → CommonCoverSolve.LinearData Q V E) (hdata : ∀ (i : I), ∀ x ∈ domains i, SameInputsAt (data i) (transportData d (φ i) (gaps i) (shift i) (rate i) (amplitude i)) (charts i x).1) (i : I) (x : X) : x ∈ domains i → (data i).commonSolve (transportGeometry g (gaps i) (shift i) (rate i) ⋯) ⋯ (κ ∘ nativeTimeMap (shift i) (rate i)) (charts i x) = amplitude i • physicalOutput d g hAB κ χ x

Existing, separately defined chart inputs produce the same single physical output as the canonical transported data when their primitive coefficient and forcing identities are verified.

Why the anchor must be transported as input data

noncomputable def NavierStokes.CopySolveCompatibility.constantForcing : CommonCoverSolve.LinearData ℝ ℝ ℝ

Constant forcing, bundling coefficient, forcingMap, source.

Equations

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

theorem NavierStokes.CopySolveCompatibility.constantForcing_anchoredSolve {a b : ℝ} (g : CommonCoverSolve.Geometry) (hab : a ≤ b) (j : TorusInverse.Frequency) (p : ℝ) (Y : TorusInverse.Plane) {s : ℝ} (hs : s ∈ Set.Icc a b) : constantForcing.anchoredSolve g hab j (p, Y) s = s - a

theorem NavierStokes.CopySolveCompatibility.changing_anchor_changes_solution (g : CommonCoverSolve.Geometry) : constantForcing.anchoredSolve g changing_anchor_changes_solution._proof_1 0 (0, 0) 0 ≠ constantForcing.anchoredSolve g changing_anchor_changes_solution._proof_2 0 (0, 0) 0

Even smooth constant source/coefficient data do not make differently anchored solves equal. This is an actual constructed-solution counterexample.