Local polar inverse of the physical residual graph

The physical radius is unscaled, while the angle is read from a valid polar chart of the scaled radial projection. The resulting cylindrical point maps back to the original Cartesian point and to the exact common graph used by the physical mean estimates.

noncomputable def NavierStokes.ResidualPolarGraph.angle (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : ℝ

The local angle of the scaled physical radial projection.

Equations

• NavierStokes.ResidualPolarGraph.angle a j n w = (NavierStokes.PolarCharts.chart a j ((NavierStokes.PhysicalGraphBounds.scaledRadial n) w)).2

noncomputable def NavierStokes.ResidualPolarGraph.cylindricalPoint (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : ProblemStatement.SpaceTime

The actual unscaled cylindrical point associated with a local polar chart. Its spatial coordinates are physical radius, angle, and axial position.

Equations

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

@[simp]

theorem NavierStokes.ResidualPolarGraph.cylindricalPoint_time (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : (cylindricalPoint a j n w).1 = w.1

@[simp]

theorem NavierStokes.ResidualPolarGraph.cylindricalPoint_radius (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : (cylindricalPoint a j n w).2.ofLp 0 = PolarCharts.radius (PhysicalGraphBounds.radialProjection w)

@[simp]

theorem NavierStokes.ResidualPolarGraph.cylindricalPoint_angle (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : (cylindricalPoint a j n w).2.ofLp 1 = angle a j n w

@[simp]

theorem NavierStokes.ResidualPolarGraph.cylindricalPoint_axial (a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : (cylindricalPoint a j n w).2.ofLp 2 = w.2.ofLp 2

theorem NavierStokes.ResidualPolarGraph.rotated_projection_pos {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : 0 < (PolarCharts.rotate j (PhysicalGraphBounds.radialProjection w)).1

theorem NavierStokes.ResidualPolarGraph.radial_projection_radius_pos {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : 0 < PolarCharts.radius (PhysicalGraphBounds.radialProjection w)

theorem NavierStokes.ResidualPolarGraph.cylindricalPoint_radius_pos {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : 0 < (cylindricalPoint a j n w).2.ofLp 0

theorem NavierStokes.ResidualPolarGraph.angle_eq_localChart {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : angle a j n w = (PolarCharts.localChart j (PhysicalGraphBounds.radialProjection w)).2

theorem NavierStokes.ResidualPolarGraph.polar_radius_angle {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : PolarCharts.polar (PolarCharts.radius (PhysicalGraphBounds.radialProjection w), angle a j n w) = PhysicalGraphBounds.radialProjection w

theorem NavierStokes.ResidualPolarGraph.chart_cylindricalPoint {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : CylindricalResidual.chart (cylindricalPoint a j n w).2 = w.2

The spatial cylindrical chart returns the original Cartesian point.

theorem NavierStokes.ResidualPolarGraph.spacetimeChart_cylindricalPoint {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : ((cylindricalPoint a j n w).1, CylindricalResidual.chart (cylindricalPoint a j n w).2) = w

The time coordinate is unchanged by the actual spatial chart.

theorem NavierStokes.ResidualPolarGraph.physicalToChartTZ_eq (h : ℝ) (n k : ℕ) : PhysicalResidualTZ.physicalToChartTZ h n k = VariableGaugeMean.physicalToChartTZ h n k

The two frozen graph interfaces use the same linear map in (T,Z) order.

theorem NavierStokes.ResidualPolarGraph.absoluteLiftTZ_cylindricalPoint (h a : ℝ) (j : PolarCharts.Index) (n : ℕ) (w : ProblemStatement.SpaceTime) : PhysicalResidualTZ.absoluteLiftTZ h (cylindricalPoint a j n w) = PhysicalMeanJetBounds.physicalPoint h w

The absolute cylindrical lift is the actual physical mean input, including its radial and time auxiliary profile.

theorem NavierStokes.ResidualPolarGraph.graphMapTZ_cylindricalPoint {a : ℝ} (ha : 0 < a) (h : ℝ) (j : PolarCharts.Index) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : PhysicalResidualTZ.graphMapTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) (cylindricalPoint a j n w) = (PhysicalMeanJetBounds.graph h n d w, angle a j n w)

Exact compatibility of the residual graph and the mean-field common cover, with the same native-index gap and the actual local chart angle.

theorem NavierStokes.ResidualPolarGraph.chart_radius_eq_graph {a : ℝ} (ha : 0 < a) (h : ℝ) (j : PolarCharts.Index) (n d : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : (PolarCharts.chart a j ((PhysicalGraphBounds.scaledRadial n) w)).1 = (PhysicalMeanJetBounds.graph h n d w).1

The radial coordinate of the scaled polar chart is exactly the first coordinate used by the physical common graph.

theorem NavierStokes.ResidualPolarGraph.eventually_chartDomain {a : ℝ} (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : ∀ᶠ (z : ProblemStatement.SpaceTime) in nhds w, (PhysicalGraphBounds.scaledRadial n) z ∈ PolarCharts.chartDomain a j

theorem NavierStokes.ResidualPolarGraph.spacetimeChart_cylindricalPoint_eventually {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : (fun (z : ProblemStatement.SpaceTime) => ((cylindricalPoint a j n z).1, CylindricalResidual.chart (cylindricalPoint a j n z).2)) =ᶠ[nhds w] id

theorem NavierStokes.ResidualPolarGraph.graphMapTZ_cylindricalPoint_eventually {a : ℝ} (ha : 0 < a) (h : ℝ) (j : PolarCharts.Index) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {w : ProblemStatement.SpaceTime} (hw : (PhysicalGraphBounds.scaledRadial n) w ∈ PolarCharts.chartDomain a j) : (fun (z : ProblemStatement.SpaceTime) => PhysicalResidualTZ.graphMapTZ (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) (cylindricalPoint a j n z)) =ᶠ[nhds w] fun (z : ProblemStatement.SpaceTime) => (PhysicalMeanJetBounds.graph h n d z, angle a j n z)