The physical residual of a scaled graph pullback

This file keeps the cylindrical angle separate from the lifted slow and fast variables. Every differential operator is an actual Frechet derivative.

noncomputable def NavierStokes.PhysicalResidualBridge.graphResidual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (a : E → Fin 3 → ℝ) (p : E → ℝ) (x : E) : Fin 3 → ℝ

The complete real graph-coordinate residual, including the quadratic transport term and the cylindrical connection terms.

Equations

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

theorem NavierStokes.PhysicalResidualBridge.along_scaled_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Γ : E → F} {V : E → E} {W : F → F} {f : F → ℝ} {x : E} (c k : ℝ) (hΓ : DifferentiableAt ℝ Γ x) (hf : DifferentiableAt ℝ f (Γ x)) (hV : (fderiv ℝ Γ x) (V x) = k • W (Γ x)) : HarmonicCalculus.along V (fun (y : E) => c * f (Γ y)) x = c * k * HarmonicCalculus.along W f (Γ x)

theorem NavierStokes.PhysicalResidualBridge.along_twice_scaled_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set E} {U : Set F} {Γ : E → F} {V : E → E} {W : F → F} {f : F → ℝ} {x : E} (c k : ℝ) (hΩ : IsOpen Ω) (hU : IsOpen U) (hΓ : ContDiffOn ℝ (↑⊤) Γ Ω) (hmap : Set.MapsTo Γ Ω U) (hW : ContDiffOn ℝ (↑⊤) W U) (hf : ContDiffOn ℝ (↑⊤) f U) (hV : ∀ y ∈ Ω, (fderiv ℝ Γ y) (V y) = k • W (Γ y)) (hx : x ∈ Ω) : HarmonicCalculus.along V (HarmonicCalculus.along V fun (y : E) => c * f (Γ y)) x = c * k ^ 2 * HarmonicCalculus.along W (HarmonicCalculus.along W f) (Γ x)

Repeating the genuine derivative differentiates the target direction field as well. In particular this includes the radial-profile derivative.

structure NavierStokes.PhysicalResidualBridge.PullbackData {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Ω : Set E) (U : Set F) (Γ : E → F) (l v : ℝ) (R : F → ℝ) (Vr Vθ Vz Vt : F → F) (Sr Sθ Sz St : E → E) (r : E → ℝ) : Prop

Differential data used by the generic pullback calculation below. The explicit physical graph later supplies every field of this structure.

• source_open : IsOpen Ω
• target_open : IsOpen U
• smooth : ContDiffOn ℝ (↑⊤) Γ Ω
• mapsTo : Set.MapsTo Γ Ω U
• radial_smooth : ContDiffOn ℝ (↑⊤) Vr U
• angular_smooth : ContDiffOn ℝ (↑⊤) Vθ U
• axial_smooth : ContDiffOn ℝ (↑⊤) Vz U
• radial (x : E) : x ∈ Ω → (fderiv ℝ Γ x) (Sr x) = l • Vr (Γ x)
• angular (x : E) : x ∈ Ω → (fderiv ℝ Γ x) (Sθ x) = Vθ (Γ x)
• axial (x : E) : x ∈ Ω → (fderiv ℝ Γ x) (Sz x) = l • Vz (Γ x)
• temporal (x : E) : x ∈ Ω → (fderiv ℝ Γ x) (St x) = (v * l) • Vt (Γ x)
• radius (x : E) : x ∈ Ω → R (Γ x) = l * r x

theorem NavierStokes.PhysicalResidualBridge.graphResidual_scaled_pull {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set E} {U : Set F} {Γ : E → F} {l v ε : ℝ} {R : F → ℝ} {Vr Vθ Vz Vt : F → F} {Sr Sθ Sz St : E → E} {r : E → ℝ} (G : PullbackData Ω U Γ l v R Vr Vθ Vz Vt Sr Sθ Sz St r) (hl : l ≠ 0) (hε : l = v * ε) {a : F → Fin 3 → ℝ} {p : F → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : F) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : E} (hx : x ∈ Ω) (hr : r x ≠ 0) (i : Fin 3) : graphResidual 1 r Sr Sθ Sz St (fun (y : E) (j : Fin 3) => v * a (Γ y) j) (fun (y : E) => v ^ 2 * p (Γ y)) x i = v ^ 2 * l * graphResidual ε R Vr Vθ Vz Vt a p (Γ x) i

theorem NavierStokes.PhysicalResidualBridge.graphResidual_eq_cylindrical {U : Set ProblemStatement.SpaceTime} {a : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hU : IsOpen U) (ha : ContDiffOn ℝ (↑⊤) a U) (hp : ContDiffOn ℝ (↑⊤) p U) (hx : (t, q) ∈ U) : graphResidual 1 LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) LinearWaveResidual.physicalTimeDirection (fun (z : ProblemStatement.SpaceTime) (i : Fin 3) => (a z).ofLp i) p (t, q) = fun (i : Fin 3) => (CylindricalResidual.cylindricalResidual a p t q).ofLp i

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualBridge.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.PhysicalResidualBridge.Plane = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualBridge.Lift : Type

Lift: an abbreviation for ℝ × (Plane × Plane).

Equations

• NavierStokes.PhysicalResidualBridge.Lift = (ℝ × NavierStokes.PhysicalResidualBridge.Plane × NavierStokes.PhysicalResidualBridge.Plane)

@[reducible, inline]

abbrev NavierStokes.PhysicalResidualBridge.Cylinder : Type

Cylinder: an abbreviation for Lift × ℝ.

Equations

• NavierStokes.PhysicalResidualBridge.Cylinder = (NavierStokes.PhysicalResidualBridge.Lift × ℝ)

structure NavierStokes.PhysicalResidualBridge.ScaledGraph : Type

Numerical and directional data of one fixed chart.

• radialScale : ℝ

  Radial scale of ScaledGraph, of type ℝ.

• velocityScale : ℝ

  Velocity scale of ScaledGraph, of type ℝ.

• epsilon : ℝ

  Epsilon of ScaledGraph, of type ℝ.

• exponent : ℝ

  Exponent of ScaledGraph, of type ℝ.

• frequency : ℝ

  Frequency of ScaledGraph, of type ℝ.

• fastCoefficient : ℝ

  Fast coefficient of ScaledGraph, of type ℝ.

• radialVector : Plane

  Radial vector of ScaledGraph, of type Plane.

• temporalVector : Plane

  Temporal vector of ScaledGraph, of type Plane.

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.map (G : ScaledGraph) (p : ProblemStatement.SpaceTime) : Cylinder

Map as an element of Cylinder.

Equations

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

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.radius (x : Cylinder) : ℝ

Radius, given by x.1.1.

Equations

• NavierStokes.PhysicalResidualBridge.ScaledGraph.radius x = x.1.1

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.radial (G : ScaledGraph) (x : Cylinder) : Cylinder

Radial, given by ((1, ((0, 0), (G.frequency * GraphCalculus.radialSpeed G.exponent x.1.1) • G.radialVector)), 0).

Equations

• G.radial x = ((1, (0, 0), (G.frequency * NavierStokes.GraphCalculus.radialSpeed G.exponent x.1.1) • G.radialVector), 0)

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.angular (_x : Cylinder) : Cylinder

Angular, given by (0, 1).

Equations

• NavierStokes.PhysicalResidualBridge.ScaledGraph.angular _x = (0, 1)

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.axial (G : ScaledGraph) (_x : Cylinder) : Cylinder

Axial, given by ((0, ((G.epsilon, 0), 0)), 0).

Equations

• G.axial _x = ((0, (G.epsilon, 0), 0), 0)

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.temporal (G : ScaledGraph) (_x : Cylinder) : Cylinder

Temporal, given by ((0, ((0, -G.epsilon), G.fastCoefficient • G.temporalVector)), 0).

Equations

• G.temporal _x = ((0, (0, -G.epsilon), G.fastCoefficient • G.temporalVector), 0)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.map_smoothAt (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) : ContDiffAt ℝ (↑⊤) G.map p

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.fderiv_map_apply (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) (w : ProblemStatement.SpaceTime) : (fderiv ℝ G.map p) w = ((G.radialScale * w.2.ofLp 0, (G.radialScale * G.epsilon * w.2.ofLp 2, -(G.velocityScale * G.radialScale * G.epsilon) * w.1), (G.frequency * GraphCalculus.radialSpeed G.exponent (G.radialScale * p.2.ofLp 0) * G.radialScale * w.2.ofLp 0) • G.radialVector + (G.velocityScale * G.radialScale * G.fastCoefficient * w.1) • G.temporalVector), w.2.ofLp 1)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.map_radial (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) : (fderiv ℝ G.map p) (LinearWaveResidual.spaceDirection 0 p) = G.radialScale • G.radial (G.map p)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.map_angular (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) : (fderiv ℝ G.map p) (LinearWaveResidual.spaceDirection 1 p) = angular (G.map p)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.map_axial (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) : (fderiv ℝ G.map p) (LinearWaveResidual.spaceDirection 2 p) = G.radialScale • G.axial (G.map p)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.map_temporal (G : ScaledGraph) {p : ProblemStatement.SpaceTime} (hr : G.radialScale * p.2.ofLp 0 ≠ 0) : (fderiv ℝ G.map p) (LinearWaveResidual.physicalTimeDirection p) = (G.velocityScale * G.radialScale) • G.temporal (G.map p)

Forward physical time produces minus the slow-time direction.

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.radial_smooth (G : ScaledGraph) {U : Set Cylinder} (hR : ∀ x ∈ U, x.1.1 ≠ 0) : ContDiffOn ℝ (↑⊤) G.radial U

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.source (G : ScaledGraph) (U : Set Cylinder) : Set ProblemStatement.SpaceTime

Source, given by {p | 0 < p.2 0} ∩ G.map ⁻¹' U.

Equations

• G.source U = {p : NavierStokes.ProblemStatement.SpaceTime | 0 < p.2.ofLp 0} ∩ G.map ⁻¹' U

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.source_open (G : ScaledGraph) (hl : 0 < G.radialScale) {U : Set Cylinder} (hU : IsOpen U) : IsOpen (G.source U)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.pullbackData (G : ScaledGraph) (hl : 0 < G.radialScale) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) : PullbackData (G.source U) U G.map G.radialScale G.velocityScale radius G.radial angular G.axial G.temporal (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) LinearWaveResidual.physicalTimeDirection LinearWaveResidual.coordinateRadius

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.velocity (G : ScaledGraph) (a : Cylinder → Fin 3 → ℝ) : ProblemStatement.VelocityField

Physical cylindrical velocity obtained from the actual graph.

Equations

• G.velocity a p = NavierStokes.AxisymmetricResidual.pack (G.velocityScale * a (G.map p) 0) (G.velocityScale * a (G.map p) 1) (G.velocityScale * a (G.map p) 2)

@[simp]

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.velocity_apply (G : ScaledGraph) (a : Cylinder → Fin 3 → ℝ) (p : ProblemStatement.SpaceTime) (i : Fin 3) : (G.velocity a p).ofLp i = G.velocityScale * a (G.map p) i

noncomputable def NavierStokes.PhysicalResidualBridge.ScaledGraph.pressure (G : ScaledGraph) (p : Cylinder → ℝ) : ProblemStatement.PressureField

Pressure, defined pointwise by G.velocityScale ^ 2 * p (G.map z).

Equations

• G.pressure p z = G.velocityScale ^ 2 * p (G.map z)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.velocity_smooth (G : ScaledGraph) (hl : 0 < G.radialScale) {U : Set Cylinder} {a : Cylinder → Fin 3 → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (z : Cylinder) => a z i) U) : ContDiffOn ℝ (↑⊤) (G.velocity a) (G.source U)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.pressure_smooth (G : ScaledGraph) (hl : 0 < G.radialScale) {U : Set Cylinder} {p : Cylinder → ℝ} (hp : ContDiffOn ℝ (↑⊤) p U) : ContDiffOn ℝ (↑⊤) (G.pressure p) (G.source U)

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.cylindricalResidual_eq (G : ScaledGraph) (hl : 0 < G.radialScale) (hε : G.radialScale = G.velocityScale * G.epsilon) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {a : Cylinder → Fin 3 → ℝ} {p : Cylinder → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : Cylinder) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {z : ProblemStatement.SpaceTime} (hz : z ∈ G.source U) (i : Fin 3) : (CylindricalResidual.cylindricalResidual (G.velocity a) (G.pressure p) z.1 z.2).ofLp i = G.velocityScale ^ 2 * G.radialScale * graphResidual G.epsilon radius G.radial angular G.axial G.temporal a p (G.map z) i

theorem NavierStokes.PhysicalResidualBridge.ScaledGraph.physical_residual (G : ScaledGraph) (hl : 0 < G.radialScale) (hε : G.radialScale = G.velocityScale * G.epsilon) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {a : Cylinder → Fin 3 → ℝ} {p : Cylinder → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : Cylinder) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ G.source U) {u : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} (hu : ContDiffAt ℝ 2 u (t, CylindricalResidual.chart q)) (hP : DifferentiableAt ℝ P (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => u (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) (G.velocity a z)) (hpRep : CylindricalResidual.pressurePullback P =ᶠ[nhds (t, q)] G.pressure p) (i : Fin 3) : ((CylindricalResidual.frame (-q.ofLp 1)) (ProblemStatement.navierStokesResidual u P t (CylindricalResidual.chart q))).ofLp i = G.velocityScale ^ 2 * G.radialScale * graphResidual G.epsilon radius G.radial angular G.axial G.temporal a p (G.map (t, q)) i

Identification with the viscosity-one Cartesian PDE. The representation premises concern only field values on a neighborhood.

noncomputable def NavierStokes.PhysicalResidualBridge.commonGraph (Q h : ℝ) (i : ℕ) : ScaledGraph

One arbitrary integer-cover chart; the index is not constrained to the native band index.

Equations

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

theorem NavierStokes.PhysicalResidualBridge.commonGraph_scale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) : (commonGraph Q h i).radialScale = (commonGraph Q h i).velocityScale * (commonGraph Q h i).epsilon

theorem NavierStokes.PhysicalResidualBridge.commonGraph_axialScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) : (commonGraph Q h i).radialScale * (commonGraph Q h i).epsilon = Q ^ (-CoordinateAlgebra.D h)

theorem NavierStokes.PhysicalResidualBridge.commonGraph_slowTimeScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) : (commonGraph Q h i).velocityScale * (commonGraph Q h i).radialScale * (commonGraph Q h i).epsilon = Q ^ (-1)

theorem NavierStokes.PhysicalResidualBridge.commonGraph_fastTimeScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) : (commonGraph Q h i).velocityScale * (commonGraph Q h i).radialScale * (commonGraph Q h i).fastCoefficient = ChartScales.Tg ^ i

theorem NavierStokes.PhysicalResidualBridge.commonGraph_radialScale {Q r : ℝ} (hQ : 0 < Q) (hr : 0 < r) (h : ℝ) (i : ℕ) : (commonGraph Q h i).frequency * ((commonGraph Q h i).radialScale * r) ^ (commonGraph Q h i).exponent = ChartScales.Lambda ^ i * r ^ ChartScales.radialExponent h

theorem NavierStokes.PhysicalResidualBridge.commonGraph_map {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) {p : ProblemStatement.SpaceTime} (hr : 0 < p.2.ofLp 0) : (commonGraph Q h i).map p = ((Q ^ (-(1 / 2)) * p.2.ofLp 0, (Q ^ (-CoordinateAlgebra.D h) * p.2.ofLp 2, (1 - p.1) / Q), (SlotGeometry.cover ^ i) (p.2.ofLp 0 ^ ChartScales.radialExponent h • PhysicalGraphBounds.radialDirection + p.1 • PhysicalGraphBounds.timeDirection)), p.2.ofLp 1)

theorem NavierStokes.PhysicalResidualBridge.commonGraph_residualScale {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (i : ℕ) : Q ^ (2 * CoordinateAlgebra.A h + 1 / 2) * ((commonGraph Q h i).velocityScale ^ 2 * (commonGraph Q h i).radialScale) = 1

theorem NavierStokes.PhysicalResidualBridge.commonGraph_physical_residual {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k : ℕ) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {a : Cylinder → Fin 3 → ℝ} {p : Cylinder → ℝ} (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : Cylinder) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ (commonGraph Q h k).source U) {u : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} (hu : ContDiffAt ℝ 2 u (t, CylindricalResidual.chart q)) (hP : DifferentiableAt ℝ P (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => u (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) ((commonGraph Q h k).velocity a z)) (hpRep : CylindricalResidual.pressurePullback P =ᶠ[nhds (t, q)] (commonGraph Q h k).pressure p) (i : Fin 3) : graphResidual (Q ^ h) ScaledGraph.radius (commonGraph Q h k).radial ScaledGraph.angular (commonGraph Q h k).axial (commonGraph Q h k).temporal a p ((commonGraph Q h k).map (t, q)) i = Q ^ (2 * CoordinateAlgebra.A h + 1 / 2) * ((CylindricalResidual.frame (-q.ofLp 1)) (ProblemStatement.navierStokesResidual u P t (CylindricalResidual.chart q))).ofLp i

The exact power multiplying the physical viscosity-one residual.

The actual linear-plus-quadratic correction expression

theorem NavierStokes.PhysicalResidualBridge.twice_along_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {V : E → E} (hV : ContDiffOn ℝ (↑⊤) V U) {f g : E → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : E} (hx : x ∈ U) : HarmonicCalculus.along V (HarmonicCalculus.along V fun (y : E) => f y + g y) x = HarmonicCalculus.along V (HarmonicCalculus.along V f) x + HarmonicCalculus.along V (HarmonicCalculus.along V g) x

theorem NavierStokes.PhysicalResidualBridge.laplacian_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (R : E → ℝ) {Vr Vθ Vz : E → E} (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {f g : E → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hg : ContDiffOn ℝ (↑⊤) g U) {x : E} (hx : x ∈ U) : HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz (fun (y : E) => f y + g y) x = HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz f x + HarmonicCalculus.cylindricalLaplacian R Vr Vθ Vz g x

theorem NavierStokes.PhysicalResidualBridge.graphResidual_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (ε : ℝ) (R : E → ℝ) {Vr Vθ Vz : E → E} (Vt : E → E) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {B a : E → Fin 3 → ℝ} {p₀ p : E → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => B y i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hp₀ : ContDiffOn ℝ (↑⊤) p₀ U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : E} (hx : x ∈ U) (i : Fin 3) : graphResidual ε R Vr Vθ Vz Vt (fun (y : E) (j : Fin 3) => B y j + a y j) (fun (y : E) => p₀ y + p y) x i = graphResidual ε R Vr Vθ Vz Vt B p₀ x i + LinearWaveResidual.realComponentLinearResidual ε R Vr Vθ Vz Vt B a p x i + LinearWaveResidual.realTransport R Vr Vθ Vz a a x i

theorem NavierStokes.PhysicalResidualBridge.transport_realLift {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) {a : E → Fin 3 → ℝ} {x : E} (ha : ∀ (j : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y j) x) (i : Fin 3) : (LinearWaveResidual.transport R Vr Vθ Vz (LinearWaveResidual.realLift a) (LinearWaveResidual.realLift a) x i).re = LinearWaveResidual.realTransport R Vr Vθ Vz a a x i

noncomputable def NavierStokes.PhysicalResidualBridge.complexIncrement {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ε : ℝ) (R : E → ℝ) (Vr Vθ Vz Vt : E → E) (B a : E → Fin 3 → ℝ) (p : E → ℝ) (x : E) (i : Fin 3) : ℝ

Complex increment as an element of ℝ.

Equations

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

theorem NavierStokes.PhysicalResidualBridge.complexIncrement_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (ε : ℝ) (R : E → ℝ) {Vr Vθ Vz : E → E} (Vt : E → E) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {B a : E → Fin 3 → ℝ} {p : E → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => B y i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : E} (hx : x ∈ U) (i : Fin 3) : complexIncrement ε R Vr Vθ Vz Vt B a p x i = LinearWaveResidual.realComponentLinearResidual ε R Vr Vθ Vz Vt B a p x i + LinearWaveResidual.realTransport R Vr Vθ Vz a a x i

theorem NavierStokes.PhysicalResidualBridge.fullResidual_eq_graph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) (ε : ℝ) (R : E → ℝ) {Vr Vθ Vz : E → E} (Vt : E → E) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) {B a : E → Fin 3 → ℝ} {p₀ p : E → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => B y i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hp₀ : ContDiffOn ℝ (↑⊤) p₀ U) (hp : ContDiffOn ℝ (↑⊤) p U) {x : E} (hx : x ∈ U) (virtual error : Fin 3 → ℝ) (hbase : ∀ (i : Fin 3), graphResidual ε R Vr Vθ Vz Vt B p₀ x i = virtual i + error i) (i : Fin 3) : complexIncrement ε R Vr Vθ Vz Vt B a p x i + virtual i + error i = graphResidual ε R Vr Vθ Vz Vt (fun (y : E) (j : Fin 3) => B y j + a y j) (fun (y : E) => p₀ y + p y) x i

The base equation supplies only the fixed base residual. All linear, quadratic, pressure, and viscous increment terms are derived above.

noncomputable def NavierStokes.PhysicalResidualBridge.absoluteLift (h : ℝ) (p : ProblemStatement.SpaceTime) : Lift

The absolute graph before choosing a band or an integer covering.

Equations

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

theorem NavierStokes.PhysicalResidualBridge.commonGraph_eq_physicalToChart (h : ℝ) (n k : ℕ) {p : ProblemStatement.SpaceTime} (hr : 0 < p.2.ofLp 0) : (commonGraph (ChartScales.Q n) h k).map p = ((MeanChartCompatibility.physicalToChart h n k) (absoluteLift h p), p.2.ofLp 1)

structure NavierStokes.PhysicalResidualBridge.MatchesAt (o : MeanIncrementBounds.Operators Lift) (G : ScaledGraph) (n : ℕ) : Prop

Matching consists of the literal coefficient and direction data at one band, with no assumption about a residual or a differential operator.

• epsilon : o.epsilon n = G.epsilon
• frequency : o.radialFrequency n = G.frequency
• fast : o.fastCoefficient n = G.fastCoefficient
• radius : o.radius = Prod.fst
• profile : o.radialProfile = fun (x : Lift) => GraphCalculus.radialSpeed G.exponent x.1
• eR : o.eR = (1, 0, 0)
• eZ : o.eZ = (0, (1, 0), 0)
• eT : o.eT = (0, (0, 1), 0)
• vR : o.vR = (0, 0, G.radialVector)
• vT : o.vT = (0, 0, G.temporalVector)

theorem NavierStokes.PhysicalResidualBridge.matchesAt_graphOperators (r : CorrectionState.ReconstructionData) (epsilon fast : ℕ → ℝ) (G : ScaledGraph) (n : ℕ) (hε : epsilon n = G.epsilon) (hM : r.frequency n = G.frequency) (hc : fast n = G.fastCoefficient) (hd : r.exponent = G.exponent) (hv : r.radialDirection = G.radialVector) : MatchesAt (CorrectionState.graphOperators r epsilon fast ((1, 0), 0) ((0, 1), 0) G.temporalVector) G n

theorem NavierStokes.PhysicalResidualBridge.MatchesAt.radialDirection {c : CorrectionState.Context Lift} {G : ScaledGraph} {n : ℕ} (H : MatchesAt c.operators G n) : LiftedMeanResidual.radialDirection c n = G.radial

theorem NavierStokes.PhysicalResidualBridge.MatchesAt.axialDirection {c : CorrectionState.Context Lift} {G : ScaledGraph} {n : ℕ} (H : MatchesAt c.operators G n) : LiftedMeanResidual.axialDirection c n = G.axial

theorem NavierStokes.PhysicalResidualBridge.MatchesAt.timeDirection {c : CorrectionState.Context Lift} {G : ScaledGraph} {n : ℕ} (H : MatchesAt c.operators G n) : LiftedMeanResidual.timeDirection c n = G.temporal

noncomputable def NavierStokes.PhysicalResidualBridge.baseComponents (c : CorrectionState.Context Lift) (n : ℕ) (x : Cylinder) : Fin 3 → ℝ

Base components, given by ![c.base.radial n x.1, c.base.angular n x.1, c.base.axial n x.1].

Equations

• NavierStokes.PhysicalResidualBridge.baseComponents c n x = ![c.base.radial n x.1, c.base.angular n x.1, c.base.axial n x.1]

noncomputable def NavierStokes.PhysicalResidualBridge.incrementComponents (s : CorrectionState.State Lift) (n : ℕ) (x : Cylinder) : Fin 3 → ℝ

Increment components, given by ![s.mean.radial n x.1 + s.oscillation n x 0, s.mean.angular n x.1 + s.oscillation n x 1, s.mean.axial n x.1 + s.oscillation n x 2].

Equations

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

theorem NavierStokes.PhysicalResidualBridge.context_fullResidual_formula {c : CorrectionState.Context Lift} {G : ScaledGraph} {n : ℕ} (H : MatchesAt c.operators G n) (s : CorrectionState.State Lift) (x : Cylinder) (i : Fin 3) : LiftedMeanResidual.fullResidual c s n x i = complexIncrement G.epsilon ScaledGraph.radius G.radial ScaledGraph.angular G.axial G.temporal (baseComponents c n) (incrementComponents s n) (s.totalPressureIncrement n) x i + LiftedMeanResidual.virtualDivergence c n x i + s.errors.base n x i

theorem NavierStokes.PhysicalResidualBridge.context_fullResidual_eq_graph {c : CorrectionState.Context Lift} {G : ScaledGraph} {n : ℕ} (H : MatchesAt c.operators G n) (s : CorrectionState.State Lift) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {p₀ : Cylinder → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Cylinder) => baseComponents c n x i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Cylinder) => incrementComponents s n x i) U) (hp₀ : ContDiffOn ℝ (↑⊤) p₀ U) (hp : ContDiffOn ℝ (↑⊤) (s.totalPressureIncrement n) U) {x : Cylinder} (hx : x ∈ U) (hbase : ∀ (i : Fin 3), graphResidual G.epsilon ScaledGraph.radius G.radial ScaledGraph.angular G.axial G.temporal (baseComponents c n) p₀ x i = LiftedMeanResidual.virtualDivergence c n x i + s.errors.base n x i) (i : Fin 3) : LiftedMeanResidual.fullResidual c s n x i = graphResidual G.epsilon ScaledGraph.radius G.radial ScaledGraph.angular G.axial G.temporal (fun (y : Cylinder) (j : Fin 3) => baseComponents c n y j + incrementComponents s n y j) (fun (y : Cylinder) => p₀ y + s.totalPressureIncrement n y) x i

Exact total-field residual for the actual correction state. The only base premise is its independently verified fixed pressure/virtual-stress equation, and the base error is included once.

theorem NavierStokes.PhysicalResidualBridge.context_fullResidual_physical {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (k n : ℕ) (c : CorrectionState.Context Lift) (s : CorrectionState.State Lift) (H : MatchesAt c.operators (commonGraph Q h k) n) {U : Set Cylinder} (hU : IsOpen U) (hR : ∀ x ∈ U, x.1.1 ≠ 0) {p₀ : Cylinder → ℝ} (hB : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Cylinder) => baseComponents c n x i) U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (x : Cylinder) => incrementComponents s n x i) U) (hp₀ : ContDiffOn ℝ (↑⊤) p₀ U) (hp : ContDiffOn ℝ (↑⊤) (s.totalPressureIncrement n) U) {t : ℝ} {q : ProblemStatement.Space} (hz : (t, q) ∈ (commonGraph Q h k).source U) (hbase : ∀ (i : Fin 3), graphResidual (Q ^ h) ScaledGraph.radius (commonGraph Q h k).radial ScaledGraph.angular (commonGraph Q h k).axial (commonGraph Q h k).temporal (baseComponents c n) p₀ ((commonGraph Q h k).map (t, q)) i = LiftedMeanResidual.virtualDivergence c n ((commonGraph Q h k).map (t, q)) i + s.errors.base n ((commonGraph Q h k).map (t, q)) i) {u : ProblemStatement.VelocityField} {P : ProblemStatement.PressureField} (hu : ContDiffAt ℝ 2 u (t, CylindricalResidual.chart q)) (hP : DifferentiableAt ℝ P (t, CylindricalResidual.chart q)) (hrep : (fun (z : ProblemStatement.SpaceTime) => u (z.1, CylindricalResidual.chart z.2)) =ᶠ[nhds (t, q)] fun (z : ℝ × ProblemStatement.Space) => (CylindricalResidual.frame (z.2.ofLp 1)) ((commonGraph Q h k).velocity (fun (y : Cylinder) (j : Fin 3) => baseComponents c n y j + incrementComponents s n y j) z)) (hpRep : CylindricalResidual.pressurePullback P =ᶠ[nhds (t, q)] (commonGraph Q h k).pressure fun (y : Cylinder) => p₀ y + s.totalPressureIncrement n y) (i : Fin 3) : LiftedMeanResidual.fullResidual c s n ((commonGraph Q h k).map (t, q)) i = Q ^ (2 * CoordinateAlgebra.A h + 1 / 2) * ((CylindricalResidual.frame (-q.ofLp 1)) (ProblemStatement.navierStokesResidual u P t (CylindricalResidual.chart q))).ofLp i

The actual correction-state residual is the scaled Cartesian Navier--Stokes residual on the physical graph. The cover index k is free. The base pressure is fixed separately because a correction state stores only pressure increments.