Physical finite prefixes of the actual correction cycle

The state and its coefficient data evolve by CorrectionStep.CycleState.iterate. At one fixed band and graph, the physical field differences below are derived from its literal four updates. Stage zero contains the base and initialization.

velocityTZ gives cylindrical components. The Cartesian realization uses the existing genuine local polar charts; its physical interpretation is asserted only on their valid domains. A final adapter accepts individual potential-curl realizations, not an assumed equality of finite prefixes.

@[reducible, inline]

abbrev NavierStokes.CyclePhysicalPrefixes.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualBridge.Cylinder.

Equations

• NavierStokes.CyclePhysicalPrefixes.Cylinder = NavierStokes.PhysicalResidualBridge.Cylinder

@[reducible, inline]

abbrev NavierStokes.CyclePhysicalPrefixes.Components : Type

Components: an abbreviation for Cylinder → Fin 3 → ℝ.

Equations

• NavierStokes.CyclePhysicalPrefixes.Components = (NavierStokes.CyclePhysicalPrefixes.Cylinder → Fin 3 → ℝ)

@[reducible, inline]

abbrev NavierStokes.CyclePhysicalPrefixes.ScaledGraph : Type

Scaled graph: an abbreviation for PhysicalResidualBridge.ScaledGraph.

Equations

• NavierStokes.CyclePhysicalPrefixes.ScaledGraph = NavierStokes.PhysicalResidualBridge.ScaledGraph

noncomputable def NavierStokes.CyclePhysicalPrefixes.velocityMap (G : ScaledGraph) : Components →ₗ[ℝ] ProblemStatement.VelocityField

The actual cylindrical realization is linear in the three components.

Equations

• NavierStokes.CyclePhysicalPrefixes.velocityMap G = { toFun := NavierStokes.PhysicalResidualTZ.velocityTZ G, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.CyclePhysicalPrefixes.pressureMap (G : ScaledGraph) : (Cylinder → ℝ) →ₗ[ℝ] ProblemStatement.PressureField

Pressure includes the square of the same fixed velocity scale.

Equations

• NavierStokes.CyclePhysicalPrefixes.pressureMap G = { toFun := NavierStokes.PhysicalResidualTZ.pressureTZ G, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.CyclePhysicalPrefixes.meanComponents (m : MeanIncrementBounds.Triple CorrectionStep.CyclePoint) (n : ℕ) : Components

Mean components, defined pointwise by ![m.radial n x.1, m.angular n x.1, m.axial n x.1].

Equations

• NavierStokes.CyclePhysicalPrefixes.meanComponents m n x = ![m.radial n x.1, m.angular n x.1, m.axial n x.1]

theorem NavierStokes.CyclePhysicalPrefixes.meanComponents_updated (m h : MeanIncrementBounds.Triple CorrectionStep.CyclePoint) (n : ℕ) : meanComponents (MeanIncrementBounds.updated m h) n = meanComponents m n + meanComponents h n

theorem NavierStokes.CyclePhysicalPrefixes.incrementComponents_eq (u : CorrectionState.State CorrectionStep.CyclePoint) (n : ℕ) : PhysicalResidualBridge.incrementComponents u n = meanComponents u.mean n + u.oscillation n

noncomputable def NavierStokes.CyclePhysicalPrefixes.cylindricalVelocity (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.VelocityField

Base plus the actual mean and oscillatory velocity, at one fixed band.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.cylindricalPressure (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.PressureField

The fixed base pressure is retained once, in addition to both state pressures.

Equations

• NavierStokes.CyclePhysicalPrefixes.cylindricalPressure G n p₀ u = (NavierStokes.CyclePhysicalPrefixes.pressureMap G) (p₀ + u.totalPressureIncrement n)

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepComponents {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (n : ℕ) : Components

All four actual velocity increments, in their order of construction.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepPressureComponents {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (n : ℕ) : Cylinder → ℝ

The four actual mean-pressure changes, and the two oscillatory pressures.

Equations

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

theorem NavierStokes.CyclePhysicalPrefixes.next_incrementComponents {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (n : ℕ) : PhysicalResidualBridge.incrementComponents (p.next v c u) n = PhysicalResidualBridge.incrementComponents u n + stepComponents p v c u n

theorem NavierStokes.CyclePhysicalPrefixes.next_pressure {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) : (p.next v c u).pressure = (p.afterRank v c u).pressure

theorem NavierStokes.CyclePhysicalPrefixes.next_pressureComponents {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (n : ℕ) : (p.next v c u).totalPressureIncrement n = u.totalPressureIncrement n + stepPressureComponents p v c u n

noncomputable def NavierStokes.CyclePhysicalPrefixes.cylindricalStepVelocity {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

Cylindrical step velocity, given by velocityMap G (stepComponents p v c u n).

Equations

• NavierStokes.CyclePhysicalPrefixes.cylindricalStepVelocity p v c u G n = (NavierStokes.CyclePhysicalPrefixes.velocityMap G) (NavierStokes.CyclePhysicalPrefixes.stepComponents p v c u n)

noncomputable def NavierStokes.CyclePhysicalPrefixes.cylindricalStepPressure {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) : ProblemStatement.PressureField

Cylindrical step pressure, given by pressureMap G (stepPressureComponents p v c u n).

Equations

• NavierStokes.CyclePhysicalPrefixes.cylindricalStepPressure p v c u G n = (NavierStokes.CyclePhysicalPrefixes.pressureMap G) (NavierStokes.CyclePhysicalPrefixes.stepPressureComponents p v c u n)

theorem NavierStokes.CyclePhysicalPrefixes.cylindricalVelocity_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) : cylindricalVelocity G n c (p.next v c u) = cylindricalVelocity G n c u + cylindricalStepVelocity p v c u G n

theorem NavierStokes.CyclePhysicalPrefixes.cylindricalPressure_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) : cylindricalPressure G n p₀ (p.next v c u) = cylindricalPressure G n p₀ u + cylindricalStepPressure p v c u G n

theorem NavierStokes.CyclePhysicalPrefixes.cylindricalVelocity_difference {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) : cylindricalVelocity G n c (p.next v c u) - cylindricalVelocity G n c u = cylindricalStepVelocity p v c u G n

theorem NavierStokes.CyclePhysicalPrefixes.cylindricalPressure_difference {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) : cylindricalPressure G n p₀ (p.next v c u) - cylindricalPressure G n p₀ u = cylindricalStepPressure p v c u G n

noncomputable def NavierStokes.CyclePhysicalPrefixes.polarVelocityMap (a : ℝ) (j : PolarCharts.Index) : ProblemStatement.VelocityField →ₗ[ℝ] ProblemStatement.VelocityField

A genuine local Cartesian realization using the frozen inverse polar chart.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.polarPressureMap (a : ℝ) (j : PolarCharts.Index) : ProblemStatement.PressureField →ₗ[ℝ] ProblemStatement.PressureField

Polar pressure map, bundling toFun, map_add, map_smul.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.velocity (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.VelocityField

The actual state velocity in this local Cartesian chart.

Equations

• NavierStokes.CyclePhysicalPrefixes.velocity a j G n c u = (NavierStokes.CyclePhysicalPrefixes.polarVelocityMap a j) (NavierStokes.CyclePhysicalPrefixes.cylindricalVelocity G n c u)

noncomputable def NavierStokes.CyclePhysicalPrefixes.pressure (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.PressureField

Pressure, given by polarPressureMap a j (cylindricalPressure G n p₀ u).

Equations

• NavierStokes.CyclePhysicalPrefixes.pressure a j G n p₀ u = (NavierStokes.CyclePhysicalPrefixes.polarPressureMap a j) (NavierStokes.CyclePhysicalPrefixes.cylindricalPressure G n p₀ u)

theorem NavierStokes.CyclePhysicalPrefixes.velocity_polar_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : velocity a j G n c u (z.1, CylindricalResidual.chart z.2) = (CylindricalResidual.frame (z.2.ofLp 1)) (cylindricalVelocity G n c u z)

theorem NavierStokes.CyclePhysicalPrefixes.pressure_polar_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (u : CorrectionState.State CorrectionStep.CyclePoint) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : pressure a j G n p₀ u (z.1, CylindricalResidual.chart z.2) = cylindricalPressure G n p₀ u z

theorem NavierStokes.CyclePhysicalPrefixes.velocity_polar_forward_germ {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : (fun (w : ProblemStatement.SpaceTime) => velocity a j G n c u (w.1, CylindricalResidual.chart w.2)) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (w.2.ofLp 1)) (cylindricalVelocity G n c u w)

The actual Cartesian realization supplies the germ used by the physical residual chart theorem, on the valid polar domain.

theorem NavierStokes.CyclePhysicalPrefixes.pressure_polar_forward_germ {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (u : CorrectionState.State CorrectionStep.CyclePoint) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : (fun (w : ProblemStatement.SpaceTime) => pressure a j G n p₀ u (w.1, CylindricalResidual.chart w.2)) =ᶠ[nhds z] cylindricalPressure G n p₀ u

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepVelocity {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

Step velocity, given by polarVelocityMap a j (cylindricalStepVelocity p v c u G n).

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepPressure {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.PressureField

Step pressure, given by polarPressureMap a j (cylindricalStepPressure p v c u G n).

Equations

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

theorem NavierStokes.CyclePhysicalPrefixes.velocity_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : velocity a j G n c (p.next v c u) = velocity a j G n c u + stepVelocity p v c u a j G n

theorem NavierStokes.CyclePhysicalPrefixes.pressure_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) : pressure a j G n p₀ (p.next v c u) = pressure a j G n p₀ u + stepPressure p v c u a j G n

theorem NavierStokes.CyclePhysicalPrefixes.velocity_difference {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : velocity a j G n c (p.next v c u) - velocity a j G n c u = stepVelocity p v c u a j G n

theorem NavierStokes.CyclePhysicalPrefixes.pressure_difference {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) : pressure a j G n p₀ (p.next v c u) - pressure a j G n p₀ u = stepPressure p v c u a j G n

The literal finite prefixes, including initialization at index zero

noncomputable def NavierStokes.CyclePhysicalPrefixes.velocityStages {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n k : ℕ) : ProblemStatement.VelocityField

Velocity stages, constructed using Nat.casesOn.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.pressureStages {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (k : ℕ) : ProblemStatement.PressureField

Pressure stages, constructed using Nat.casesOn.

Equations

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

@[simp]

theorem NavierStokes.CyclePhysicalPrefixes.velocityStages_zero {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : velocityStages p c seed a j G n 0 = velocity a j G n c seed.state

@[simp]

theorem NavierStokes.CyclePhysicalPrefixes.pressureStages_zero {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) : pressureStages p c seed a j G n p₀ 0 = pressure a j G n p₀ seed.state

theorem NavierStokes.CyclePhysicalPrefixes.velocity_prefix {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n J : ℕ) : DiagonalJetBounds.uncutPrefix (velocityStages p c seed a j G n) (J + 1) = velocity a j G n c (CorrectionStep.CycleState.iterate p c seed J).state

theorem NavierStokes.CyclePhysicalPrefixes.pressure_prefix {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (p₀ : Cylinder → ℝ) (J : ℕ) : DiagonalJetBounds.uncutPrefix (pressureStages p c seed a j G n p₀) (J + 1) = pressure a j G n p₀ (CorrectionStep.CycleState.iterate p c seed J).state

The actual split into potential and direct angular contributions

noncomputable def NavierStokes.CyclePhysicalPrefixes.meridionalComponents (m : MeanIncrementBounds.Triple CorrectionStep.CyclePoint) (n : ℕ) : Components

Meridional components, defined pointwise by ![m.radial n x.1, 0, m.axial n x.1].

Equations

• NavierStokes.CyclePhysicalPrefixes.meridionalComponents m n x = ![m.radial n x.1, 0, m.axial n x.1]

noncomputable def NavierStokes.CyclePhysicalPrefixes.angularComponents (m : MeanIncrementBounds.Triple CorrectionStep.CyclePoint) (n : ℕ) : Components

Angular components, defined pointwise by ![0, m.angular n x.1, 0].

Equations

• NavierStokes.CyclePhysicalPrefixes.angularComponents m n x = ![0, m.angular n x.1, 0]

theorem NavierStokes.CyclePhysicalPrefixes.meanComponents_split (m : MeanIncrementBounds.Triple CorrectionStep.CyclePoint) (n : ℕ) : meanComponents m n = meridionalComponents m n + angularComponents m n

noncomputable def NavierStokes.CyclePhysicalPrefixes.initialPotentialPart (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.VelocityField

This velocity contribution still needs a potential realization. It includes the full base, the initialized wave, and the meridional mean.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.initialDirectPart (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (u : CorrectionState.State CorrectionStep.CyclePoint) : ProblemStatement.VelocityField

Initial direct part, given by polarVelocityMap a j (velocityMap G (angularComponents u.mean n)).

Equations

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

theorem NavierStokes.CyclePhysicalPrefixes.velocity_initial_split (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) : velocity a j G n c u = initialPotentialPart a j G n c u + initialDirectPart a j G n u

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepPotentialPart {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

The wave increments and the two meridional mean increments, literally.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.stepDirectPart {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

The angular means remain direct velocities, not unspecified curls.

Equations

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

theorem NavierStokes.CyclePhysicalPrefixes.stepVelocity_split {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (u : CorrectionState.State CorrectionStep.CyclePoint) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : stepVelocity p v c u a j G n = stepPotentialPart p v c u a j G n + stepDirectPart p v c u a j G n

noncomputable def NavierStokes.CyclePhysicalPrefixes.potentialParts {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n k : ℕ) : ProblemStatement.VelocityField

The exact velocity each still-to-be-constructed potential must realize.

Equations

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

noncomputable def NavierStokes.CyclePhysicalPrefixes.directStages {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n k : ℕ) : ProblemStatement.VelocityField

The direct angular sequence is constructed from the actual states.

Equations

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

theorem NavierStokes.CyclePhysicalPrefixes.velocityStages_split {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n k : ℕ) : velocityStages p c seed a j G n k = potentialParts p c seed a j G n k + directStages p c seed a j G n k

theorem NavierStokes.CyclePhysicalPrefixes.curl_uncutPrefix {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (A k) U) (N : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : SpatialCurl.spatialCurl (DiagonalJetBounds.uncutPrefix A N) z = ∑ k ∈ Finset.range N, SpatialCurl.spatialCurl (A k) z

The linearity of the genuine spatial derivative in the finite potential sum. Only local first differentiability is needed for this identity.

theorem NavierStokes.CyclePhysicalPrefixes.mixedVelocity_prefix {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (A k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (A k)) (potentialParts p c seed a j G n k) U) (J : ℕ) : Set.EqOn (MixedDiagonalResidual.uncutVelocity A (directStages p c seed a j G n) J) (velocity a j G n c (CorrectionStep.CycleState.iterate p c seed J).state) U

No prefix matching is assumed: individual curl realizations give the actual finite state, with its initialized index zero and literal direct means.

theorem NavierStokes.CyclePhysicalPrefixes.mixedResidual_prefix {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (A k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (A k)) (potentialParts p c seed a j G n k) U) (p₀ : Cylinder → ℝ) (J : ℕ) : Set.EqOn (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (MixedDiagonalResidual.uncutVelocity A (directStages p c seed a j G n) J) (DiagonalJetBounds.uncutPrefix (pressureStages p c seed a j G n p₀) (J + 1)) z.1 z.2) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (velocity a j G n c (CorrectionStep.CycleState.iterate p c seed J).state) (pressure a j G n p₀ (CorrectionStep.CycleState.iterate p c seed J).state) z.1 z.2) U

The actual nonlinear residuals agree locally, as a consequence of the proved finite velocity/pressure identities. No residual estimate is assumed.

theorem NavierStokes.CyclePhysicalPrefixes.mixedResidual_prefix_jets {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context CorrectionStep.CyclePoint) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (k : ℕ), DifferentiableOn ℝ (A k) U) (hcurl : ∀ (k : ℕ), Set.EqOn (SpatialCurl.spatialCurl (A k)) (potentialParts p c seed a j G n k) U) (p₀ : Cylinder → ℝ) (J m : ℕ) : Set.EqOn (iteratedFDeriv ℝ m fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (MixedDiagonalResidual.uncutVelocity A (directStages p c seed a j G n) J) (DiagonalJetBounds.uncutPrefix (pressureStages p c seed a j G n p₀) (J + 1)) z.1 z.2) (iteratedFDeriv ℝ m fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (velocity a j G n c (CorrectionStep.CycleState.iterate p c seed J).state) (pressure a j G n p₀ (CorrectionStep.CycleState.iterate p c seed J).state) z.1 z.2) U

The same equality holds for every genuine joint spacetime derivative.