Naturality of the actual mean operators

Radial endpoints, the normalized density, the compactification cutoff, frequencies, and amplitudes are transported together. The identities below are identities of the defined integral/Fourier/rank operators, not an assumption that separately chosen chart outputs coincide.

theorem NavierStokes.MeanChartCompatibility.cutoff_scale {l : ℝ} (hl : l ≠ 0) (a b x : ℝ) : TransportPrimitive.cutoff (l * a) (l * b) (l * x) = TransportPrimitive.cutoff a b x

theorem NavierStokes.MeanChartCompatibility.interiorCutoff_scale {l : ℝ} (hl : l ≠ 0) (a b x : ℝ) : TransportPrimitive.interiorCutoff (l * a) (l * b) (l * x) = TransportPrimitive.interiorCutoff a b x

theorem NavierStokes.MeanChartCompatibility.interiorCutoff_power_scale {l a b x : ℝ} (hl : 0 < l) (ha : 0 ≤ a) (hb : 0 ≤ b) (hx : 0 ≤ x) (d : ℝ) : TransportPrimitive.interiorCutoff ((l * a) ^ d) ((l * b) ^ d) ((l * x) ^ d) = TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (x ^ d)

theorem NavierStokes.MeanChartCompatibility.meanBump_scale {l a b : ℝ} (hl : 0 < l) (hab : a < b) (x : ℝ) : ↑(PressureStream.meanBump (l * a) (l * b) ⋯) (l * x) = ↑(PressureStream.meanBump a b hab) x

theorem NavierStokes.MeanChartCompatibility.meanBump_integral_scale {l a b : ℝ} (hl : 0 < l) (hab : a < b) : ∫ (x : ℝ), ↑(PressureStream.meanBump (l * a) (l * b) ⋯) x = l * ∫ (x : ℝ), ↑(PressureStream.meanBump a b hab) x

theorem NavierStokes.MeanChartCompatibility.rho_scale {l a b : ℝ} (hl : 0 < l) (hab : a < b) (x : ℝ) : PressureStream.rho (l * a) (l * b) ⋯ (l * x) = l⁻¹ * PressureStream.rho a b hab x

The density transforms with the inverse radial length.

noncomputable def NavierStokes.MeanChartCompatibility.chartLinear {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) : ℝ × E →L[ℝ] ℝ × F

Chart linear, given by (l • ContinuousLinearMap.id ℝ ℝ).prodMap C.

Equations

• NavierStokes.MeanChartCompatibility.chartLinear l C = (l • ContinuousLinearMap.id ℝ ℝ).prodMap C

@[simp]

theorem NavierStokes.MeanChartCompatibility.chartLinear_apply {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (z : ℝ × E) : (chartLinear l C) z = (l * z.1, C z.2)

noncomputable def NavierStokes.MeanChartCompatibility.pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u : ℝ) (f : ℝ × F → ℝ) (z : ℝ × E) : ℝ

Pull, given by u * f (chartLinear l C z).

Equations

• NavierStokes.MeanChartCompatibility.pull l C u f z = u * f ((NavierStokes.MeanChartCompatibility.chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.pull_smooth {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u : ℝ) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (pull l C u f)

theorem NavierStokes.MeanChartCompatibility.pull_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b : ℝ} (hl : 0 < l) (C : E →L[ℝ] F) (u : ℝ) {f : ℝ × F → ℝ} (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) : RadialAlias.RadiallySupported a b (pull l C u f)

theorem NavierStokes.MeanChartCompatibility.shifted_chart {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : ℝ} (hl : 0 < l) (C : E →L[ℝ] F) (d M N : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) {r s : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) (Y : E) : C (Y + (M * (s ^ d - r ^ d)) • v) = C Y + (N * ((l * s) ^ d - (l * r) ^ d)) • w

theorem NavierStokes.MeanChartCompatibility.shifted_integral_scale {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a t r : ℝ} (hl : 0 < l) (ha : 0 ≤ a) (hat : a ≤ t) (hr : 0 ≤ r) (C : E →L[ℝ] F) (d M N u : ℝ) (v : E) (w : F) (f : ℝ × F → ℝ) (Y : E) (hshift : M • C v = (N * l ^ d) • w) : ∫ (s : ℝ) in a..t, pull l C u f (s, Y + (M * (s ^ d - r ^ d)) • v) = u / l * ∫ (x : ℝ) in l * a..l * t, f (x, C Y + (N * (x ^ d - (l * r) ^ d)) • w)

theorem NavierStokes.MeanChartCompatibility.physicalCompact_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (C : E →L[ℝ] F) (M N u : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) : RadialPullback.physicalCompact d a b M v (pull l C u f) z = u / l * RadialPullback.physicalCompact d (l * a) (l * b) N w f ((chartLinear l C) z)

Scaling of the actual compact radial integral, with transformed endpoints and the exact transformed transport direction.

theorem NavierStokes.MeanChartCompatibility.weightedSource_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : ℝ} (hl : l ≠ 0) (C : E →L[ℝ] F) (u : ℝ) (f : ℝ × F → ℝ) : PressureStream.weightedSource (pull l C u f) = pull l C (u / l) (PressureStream.weightedSource f)

theorem NavierStokes.MeanChartCompatibility.streamPotential_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (C : E →L[ℝ] F) (M N u : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) : PressureStream.streamPotential d a b M v (pull l C u f) = pull l C (u / l) (PressureStream.streamPotential d (l * a) (l * b) N w f)

The stream potential has one less velocity length factor.

theorem NavierStokes.MeanChartCompatibility.fderiv_pull_apply {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u : ℝ) {f : ℝ × F → ℝ} {z : ℝ × E} (hf : DifferentiableAt ℝ f ((chartLinear l C) z)) (v : ℝ × E) : (fderiv ℝ (pull l C u f) z) v = u * (fderiv ℝ f ((chartLinear l C) z)) ((chartLinear l C) v)

theorem NavierStokes.MeanChartCompatibility.divideRadius_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : ℝ} (hl : l ≠ 0) (C : E →L[ℝ] F) (u : ℝ) (f : ℝ × F → ℝ) (z : ℝ × E) : PressureStream.divideRadius (pull l C u f) z = u * l * PressureStream.divideRadius f ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.graphDr_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u : ℝ) (knew kold : ℝ → ℝ) (v : E) (w : F) {f : ℝ × F → ℝ} {z : ℝ × E} (hf : DifferentiableAt ℝ f ((chartLinear l C) z)) (hvector : C (knew z.1 • v) = l • kold (l * z.1) • w) : PressureStream.graphDr knew v (pull l C u f) z = u * l * PressureStream.graphDr kold w f ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.graphDz_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u k : ℝ) (v : E) (w : F) {f : ℝ × F → ℝ} {z : ℝ × E} (hf : DifferentiableAt ℝ f ((chartLinear l C) z)) (hvector : C v = k • w) : PressureStream.graphDz v (pull l C u f) z = u * k * PressureStream.graphDz w f ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.physicalSpeed_vector {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l R : ℝ} (hl : 0 < l) (hR : 0 ≤ R) (C : E →L[ℝ] F) (d M N : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) : C (PressureStream.physicalSpeed d M R • v) = l • PressureStream.physicalSpeed d N (l * R) • w

theorem NavierStokes.MeanChartCompatibility.streamGamma_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : ℝ} (hl : l ≠ 0) (C : E →L[ℝ] F) (u : ℝ) (knew kold : ℝ → ℝ) (v : E) (w : F) {f : ℝ × F → ℝ} {z : ℝ × E} (hf : DifferentiableAt ℝ f ((chartLinear l C) z)) (hvector : C (knew z.1 • v) = l • kold (l * z.1) • w) : PressureStream.streamGamma knew v (pull l C u f) z = u * l * PressureStream.streamGamma kold w f ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.streamBeta_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (l : ℝ) (C : E →L[ℝ] F) (u k : ℝ) (v : E) (w : F) {f : ℝ × F → ℝ} {z : ℝ × E} (hf : DifferentiableAt ℝ f ((chartLinear l C) z)) (hvector : C v = k • w) : PressureStream.streamBeta v (pull l C u f) z = u * k * PressureStream.streamBeta w f ((chartLinear l C) z)

noncomputable def NavierStokes.MeanChartCompatibility.parameterPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (u : ℝ) (f : PressureStream.Lift T → ℝ) : PressureStream.Lift S → ℝ

Parameter pull, given by pull l (P.prodMap (ContinuousLinearMap.id ℝ Plane)) u f.

Equations

• NavierStokes.MeanChartCompatibility.parameterPull l P u f = NavierStokes.MeanChartCompatibility.pull l (P.prodMap (ContinuousLinearMap.id ℝ NavierStokes.TorusInverse.Plane)) u f

noncomputable def NavierStokes.MeanChartCompatibility.coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) (f : PressureStream.Lift T → ℝ) : PressureStream.Lift S → ℝ

Cover pull, given by pull l (P.prodMap (TemporalMeanUpdate.coverMap k)) u f.

Equations

• NavierStokes.MeanChartCompatibility.coverPull l P k u f = NavierStokes.MeanChartCompatibility.pull l (P.prodMap (NavierStokes.TemporalMeanUpdate.coverMap k)) u f

theorem NavierStokes.MeanChartCompatibility.coverPull_eq {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) (f : PressureStream.Lift T → ℝ) : coverPull l P k u f = TemporalMeanUpdate.pullbackCover k (parameterPull l P u f)

theorem NavierStokes.MeanChartCompatibility.parameterPull_smooth {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (parameterPull l P u f)

theorem NavierStokes.MeanChartCompatibility.parameterPull_periodic {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (parameterPull l P u f)

theorem NavierStokes.MeanChartCompatibility.coverPull_smooth {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (coverPull l P k u f)

theorem NavierStokes.MeanChartCompatibility.coverPull_periodic {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hp : PressureStream.TorusPeriodicLift f) : PressureStream.TorusPeriodicLift (coverPull l P k u f)

theorem NavierStokes.MeanChartCompatibility.torusAverage_parameterPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (u : ℝ) (f : PressureStream.Lift T → ℝ) (p : ℝ × S) : PressureStream.torusAverage (parameterPull l P u f) p = u * PressureStream.torusAverage f (l * p.1, P p.2)

theorem NavierStokes.MeanChartCompatibility.torusAverage_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (p : ℝ × S) : PressureStream.torusAverage (coverPull l P k u f) p = u * PressureStream.torusAverage f (l * p.1, P p.2)

theorem NavierStokes.MeanChartCompatibility.pressureMass_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (s : S) : PressureStream.pressureMass (coverPull l P k u f) s = u / l * PressureStream.pressureMass f (P s)

theorem NavierStokes.MeanChartCompatibility.pressureSource_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l a b : ℝ} (hl : 0 < l) (hab : a < b) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : PressureStream.pressureSource a b hab (coverPull l P k u f) = coverPull l P k u (PressureStream.pressureSource (l * a) (l * b) ⋯ f)

theorem NavierStokes.MeanChartCompatibility.centered_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : TemporalMeanUpdate.centered (coverPull l P k u f) = coverPull l P k u (TemporalMeanUpdate.centered f)

theorem NavierStokes.MeanChartCompatibility.meanPressure_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (P : S →L[ℝ] T) (k : ℕ) (M N u : ℝ) (v w : TorusInverse.Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : PressureStream.Lift S) : PressureStream.meanPressure d a b M hab v (coverPull l P k u f) z = coverPull l P k (u / l) (PressureStream.meanPressure d (l * a) (l * b) N ⋯ w f) z

Naturality of the actual pressure formula, including its normalized mass correction and compactification, on a common covering.

theorem NavierStokes.MeanChartCompatibility.absoluteInverse_const_mul (c : ℂ) (f : TorusInverse.Plane → ℂ) (Y : TorusInverse.Plane) : TemporalMeanUpdate.absoluteInverse (fun (z : TorusInverse.Plane) => c * f z) Y = c * TemporalMeanUpdate.absoluteInverse f Y

theorem NavierStokes.MeanChartCompatibility.temporalInverse_parameterPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (u : ℝ) (f : PressureStream.Lift T → ℝ) (z : PressureStream.Lift S) : TemporalMeanUpdate.temporalInverse (parameterPull l P u f) z = parameterPull l P u (TemporalMeanUpdate.temporalInverse f) z

theorem NavierStokes.MeanChartCompatibility.temporalInverse_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hm : ∀ (p : ℝ × T), PressureStream.torusAverage f p = 0) (z : PressureStream.Lift S) : TemporalMeanUpdate.temporalInverse (coverPull l P k u f) z = (ChartScales.Tg ^ k)⁻¹ * coverPull l P k u (TemporalMeanUpdate.temporalInverse f) z

theorem NavierStokes.MeanChartCompatibility.temporalInverse_centered_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (l : ℝ) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : TemporalMeanUpdate.temporalInverse (TemporalMeanUpdate.centered (coverPull l P k u f)) z = (ChartScales.Tg ^ k)⁻¹ * coverPull l P k u (TemporalMeanUpdate.temporalInverse (TemporalMeanUpdate.centered f)) z

theorem NavierStokes.MeanChartCompatibility.temporal_physical_pull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (h : ℝ) (n : ℕ) (l : ℝ) (P : S →L[ℝ] T) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : coverPull l P (ChartScales.nativeIndex h n) (ChartScales.Q n ^ (-CoordinateAlgebra.A h)) (TemporalMeanUpdate.desiredIncrement h n f) z = -TemporalMeanUpdate.temporalInverse (TemporalMeanUpdate.centered (coverPull l P (ChartScales.nativeIndex h n) (ChartScales.Q n ^ (-(2 * CoordinateAlgebra.A h + 1 / 2))) f)) z

The physical temporal update is one fixed Fourier operator. The native cover factor and the momentum/velocity unit factors cancel exactly.

noncomputable def NavierStokes.MeanChartCompatibility.temporalAtIndex {S : Type} (h : ℝ) (n i : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

The common-index form of the actual temporal update. A common index is independent of the dyadic band; the native recipe is its specialization.

Equations

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

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_native {S : Type} (h : ℝ) (n : ℕ) (f : PressureStream.Lift S → ℝ) : temporalAtIndex h n (ChartScales.nativeIndex h n) f = TemporalMeanUpdate.desiredIncrement h n f

noncomputable def NavierStokes.MeanChartCompatibility.physicalTemporal {S : Type} (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Physical temporal, given by -TemporalMeanUpdate.temporalInverse (TemporalMeanUpdate.centered f) z.

Equations

• NavierStokes.MeanChartCompatibility.physicalTemporal f z = -NavierStokes.TemporalMeanUpdate.temporalInverse (NavierStokes.TemporalMeanUpdate.centered f) z

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_physical_pull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] (h : ℝ) (n i : ℕ) (l : ℝ) (P : S →L[ℝ] T) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : coverPull l P i (ChartScales.Q n ^ (-CoordinateAlgebra.A h)) (temporalAtIndex h n i f) z = physicalTemporal (coverPull l P i (ChartScales.Q n ^ (-(2 * CoordinateAlgebra.A h + 1 / 2))) f) z

All common indices give the same physical temporal operator after the actual velocity and momentum normalizations.

theorem NavierStokes.MeanChartCompatibility.normalizeDebt_scale {l u ell U : ℝ} (hl : l ≠ 0) (hu : u ≠ 0) (hell : ell ≠ 0) (hU : U ≠ 0) (d : MeanRankUpdate.Debt) : MeanRankUpdate.normalizeDebt (l * ell) (u * U) (MeanRankUpdate.scaleDebt l u d) = MeanRankUpdate.normalizeDebt ell U d

theorem NavierStokes.MeanChartCompatibility.rankAngular_scale {l u ell U : ℝ} (hl : l ≠ 0) (hu : u ≠ 0) (hell : ell ≠ 0) (hU : U ≠ 0) (lam C a b : ℝ) (d : MeanRankUpdate.Debt) (r : ℝ) : MeanRankUpdate.angularIncrement lam C a b (l * ell) (u * U) (MeanRankUpdate.scaleDebt l u d) (l * r) = u * MeanRankUpdate.angularIncrement lam C a b ell U d r

Naturality of the constructed five-row inverse, not just of its rows.

theorem NavierStokes.MeanChartCompatibility.rankDesiredAxial_scale {l u ell U : ℝ} (hl : l ≠ 0) (hu : u ≠ 0) (hell : ell ≠ 0) (hU : U ≠ 0) (lam C a b : ℝ) (d : MeanRankUpdate.Debt) (r : ℝ) : MeanRankUpdate.desiredAxialIncrement lam C a b (l * ell) (u * U) (MeanRankUpdate.scaleDebt l u d) (l * r) = u * MeanRankUpdate.desiredAxialIncrement lam C a b ell U d r

theorem NavierStokes.MeanChartCompatibility.rankBackground_scale {l : ℝ} (hl : l ≠ 0) (u ell U lam C r : ℝ) : MeanRankUpdate.background lam C (l * ell) (u * U) (l * r) = u * MeanRankUpdate.background lam C ell U r

noncomputable def NavierStokes.MeanChartCompatibility.commonRatio (h : ℝ) (n i : ℕ) : ℝ

Common ratio, given by ChartScales.Tg ^ ChartScales.nativeIndex h n / ChartScales.Tg ^ i.

Equations

• NavierStokes.MeanChartCompatibility.commonRatio h n i = NavierStokes.ChartScales.Tg ^ NavierStokes.ChartScales.nativeIndex h n / NavierStokes.ChartScales.Tg ^ i

theorem NavierStokes.MeanChartCompatibility.commonRatio_pos (h : ℝ) (n i : ℕ) : 0 < commonRatio h n i

theorem NavierStokes.MeanChartCompatibility.commonRatio_le {h : ℝ} {n i D : ℕ} (hgap : ChartScales.nativeIndex h n ≤ i + D) : commonRatio h n i ≤ ChartScales.Tg ^ D

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_eq_native {S : Type} (h : ℝ) (n i : ℕ) (f : PressureStream.Lift S → ℝ) : temporalAtIndex h n i f = fun (z : PressureStream.Lift S) => commonRatio h n i * TemporalMeanUpdate.desiredIncrement h n f z

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_periodic {S : Type} (h : ℝ) (n i : ℕ) (f : PressureStream.Lift S → ℝ) : PressureStream.TorusPeriodicLift (temporalAtIndex h n i f)

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_supported {S : Type} (h : ℝ) (n i : ℕ) {a b : ℝ} {f : PressureStream.Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (temporalAtIndex h n i f)

theorem NavierStokes.MeanChartCompatibility.meanClass_temporalAtIndex_of_native {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (s : WeightedClasses.StripData (PressureStream.Lift S)) {h α : ℝ} {f : ℕ → PressureStream.Lift S → ℝ} (index : ℕ → ℕ) (D : ℕ) (hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + D) (hf : WeightedClasses.MeanClass s α fun (n : ℕ) => TemporalMeanUpdate.desiredIncrement h n (f n)) : WeightedClasses.MeanClass s α fun (n : ℕ) => temporalAtIndex h n (index n) (f n)

noncomputable def NavierStokes.MeanChartCompatibility.fastAtIndex {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (h : ℝ) (n i : ℕ) (f : PressureStream.Lift S → ℝ) (z : PressureStream.Lift S) : ℝ

Fast at index, given by (ChartScales.Tg ^ i * ChartScales.Q n ^ (1 + h)) * PressureStream.graphDz ((0 : S), vector .temporal) f z.

Equations

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

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n i : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) : ContDiff ℝ (↑⊤) (temporalAtIndex h n i f)

theorem NavierStokes.MeanChartCompatibility.temporalAtIndex_fast_cancellation {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (h : ℝ) (n i : ℕ) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (z : PressureStream.Lift S) : fastAtIndex h n i (temporalAtIndex h n i f) z = -TemporalMeanUpdate.centered f z

theorem NavierStokes.MeanChartCompatibility.coverMap_eq_coverPower (i : ℕ) (Y : TorusInverse.Plane) : (TemporalMeanUpdate.coverMap i) Y = (CommonCoverSolve.coverPower i) Y

theorem NavierStokes.MeanChartCompatibility.coverMap_radial (i : ℕ) : (TemporalMeanUpdate.coverMap i) (TorusInverse.vector TorusInverse.Direction.radial) = ChartScales.Lambda ^ i • TorusInverse.vector TorusInverse.Direction.radial

noncomputable def NavierStokes.MeanChartCompatibility.chartScale (n : ℕ) : ℝ

Chart scale, given by ChartScales.Q n ^ (-(1 / 2 : ℝ)).

Equations

• NavierStokes.MeanChartCompatibility.chartScale n = NavierStokes.ChartScales.Q n ^ (-(1 / 2))

theorem NavierStokes.MeanChartCompatibility.chartScale_pos (n : ℕ) : 0 < chartScale n

noncomputable def NavierStokes.MeanChartCompatibility.radialFrequency (_h : ℝ) (n i : ℕ) (d M : ℝ) : ℝ

Radial frequency, given by M * ChartScales.Lambda ^ i * ChartScales.Q n ^ (d / 2).

Equations

• NavierStokes.MeanChartCompatibility.radialFrequency _h n i d M = M * NavierStokes.ChartScales.Lambda ^ i * NavierStokes.ChartScales.Q n ^ (d / 2)

theorem NavierStokes.MeanChartCompatibility.radialFrequency_scale (h : ℝ) (n i : ℕ) (d M : ℝ) : radialFrequency h n i d M * chartScale n ^ d = M * ChartScales.Lambda ^ i

theorem NavierStokes.MeanChartCompatibility.radialFrequency_native (h : ℝ) (n : ℕ) : radialFrequency h n (ChartScales.nativeIndex h n) (ChartScales.radialExponent h) 1 = ChartScales.radialCoefficient h n

theorem NavierStokes.MeanChartCompatibility.radialFrequency_shift (h : ℝ) (n i : ℕ) (d M : ℝ) : M • (TemporalMeanUpdate.coverMap i) (TorusInverse.vector TorusInverse.Direction.radial) = (radialFrequency h n i d M * chartScale n ^ d) • TorusInverse.vector TorusInverse.Direction.radial

noncomputable def NavierStokes.MeanChartCompatibility.slowToChart (h : ℝ) (n : ℕ) : TorusInverse.Plane →L[ℝ] TorusInverse.Plane

The physical slow variables are (z,τ) with τ=1-t.

Equations

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

noncomputable def NavierStokes.MeanChartCompatibility.physicalToChart (h : ℝ) (n i : ℕ) : PressureStream.Lift TorusInverse.Plane →L[ℝ] PressureStream.Lift TorusInverse.Plane

Physical to chart, given by chartLinear (chartScale n) ((slowToChart h n).prodMap (TemporalMeanUpdate.coverMap i)).

Equations

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

@[simp]

theorem NavierStokes.MeanChartCompatibility.physicalToChart_apply (h : ℝ) (n i : ℕ) (z : PressureStream.Lift TorusInverse.Plane) : (physicalToChart h n i) z = (chartScale n * z.1, (ChartScales.Q n ^ (-CoordinateAlgebra.D h) * z.2.1.1, ChartScales.Q n ^ (-1) * z.2.1.2), (TemporalMeanUpdate.coverMap i) z.2.2)

noncomputable def NavierStokes.MeanChartCompatibility.fieldOnPhysical (h : ℝ) (n i : ℕ) (a : ℝ) (f : PressureStream.Lift TorusInverse.Plane → ℝ) : PressureStream.Lift TorusInverse.Plane → ℝ

Normalize a chart field of scaling degree a on the actual physical slow variables and absolute auxiliary lift.

Equations

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

theorem NavierStokes.MeanChartCompatibility.fieldOnPhysical_apply (h : ℝ) (n i : ℕ) (a : ℝ) (f : PressureStream.Lift TorusInverse.Plane → ℝ) (z : PressureStream.Lift TorusInverse.Plane) : fieldOnPhysical h n i a f z = ChartScales.Q n ^ (-a) * f ((physicalToChart h n i) z)

theorem NavierStokes.MeanChartCompatibility.pressure_unit_factor (h : ℝ) (n : ℕ) : ChartScales.Q n ^ (-(2 * CoordinateAlgebra.A h + 1 / 2)) / chartScale n = ChartScales.Q n ^ (-(2 * CoordinateAlgebra.A h))

noncomputable def NavierStokes.MeanChartCompatibility.bandReconstruction (h : ℝ) (n i : ℕ) (d a b M : ℝ) (hab : a < b) : CorrectionState.ReconstructionData

A chart-specific instance of the existing reconstruction recipe. The physical endpoints and frequency are transported, rather than copied.

Equations

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

theorem NavierStokes.MeanChartCompatibility.physicalPressure_naturality {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (h : ℝ) (n i : ℕ) (M : ℝ) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported (chartScale n * a) (chartScale n * b) f) : PressureStream.meanPressure d a b M hab (TorusInverse.vector TorusInverse.Direction.radial) (fieldOnPhysical h n i (2 * CoordinateAlgebra.A h + 1 / 2) f) = fieldOnPhysical h n i (2 * CoordinateAlgebra.A h) (PressureStream.meanPressure d (chartScale n * a) (chartScale n * b) (radialFrequency h n i d M) ⋯ (TorusInverse.vector TorusInverse.Direction.radial) f)

The normalized chart pressure is exactly one physical pressure operator applied to the normalized radial source.

noncomputable def NavierStokes.MeanChartCompatibility.reconstructPressureFamily (r : ℕ → CorrectionState.ReconstructionData) (c : CorrectionState.Context (PressureStream.Lift TorusInverse.Plane)) (u : CorrectionState.State (PressureStream.Lift TorusInverse.Plane)) : CorrectionState.State (PressureStream.Lift TorusInverse.Plane)

Reconstruct pressure family, given by { u with pressure := fun n => (CorrectionState.reconstructPressure (r n) c u).pressure n }.

Equations

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

theorem NavierStokes.MeanChartCompatibility.reconstructPressureFamily_represents {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (h M : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context (PressureStream.Lift TorusInverse.Plane)) (u : CorrectionState.State (PressureStream.Lift TorusInverse.Plane)) (F : PressureStream.Lift TorusInverse.Plane → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (u.gr c n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (u.gr c n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported (chartScale n * a) (chartScale n * b) (u.gr c n)) (hsource : ∀ (n : ℕ), fieldOnPhysical h n (index n) (2 * CoordinateAlgebra.A h + 1 / 2) (u.gr c n) = F) (n : ℕ) : fieldOnPhysical h n (index n) (2 * CoordinateAlgebra.A h) ((reconstructPressureFamily (fun (k : ℕ) => bandReconstruction h k (index k) d a b M hab) c u).pressure n) = PressureStream.meanPressure d a b M hab (TorusInverse.vector TorusInverse.Direction.radial) F

If the normalized sources are one physical source, the recomputed pressures are representations of its single, defined physical pressure. Compatibility of the output is the conclusion, not an input.

theorem NavierStokes.MeanChartCompatibility.temporalFamily_represents (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift TorusInverse.Plane → ℝ) (F : PressureStream.Lift TorusInverse.Plane → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (f n)) (hsource : ∀ (n : ℕ), fieldOnPhysical h n (index n) (2 * CoordinateAlgebra.A h + 1 / 2) (f n) = F) (n : ℕ) : fieldOnPhysical h n (index n) (CoordinateAlgebra.A h) (temporalAtIndex h n (index n) (f n)) = physicalTemporal F

theorem NavierStokes.MeanChartCompatibility.reconstructedGamma_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (C : E →L[ℝ] F) (M N u : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) (hz : 0 ≤ z.1) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) v (PressureStream.streamPotential d a b M v (pull l C u f)) z = u * PressureStream.streamGamma (PressureStream.physicalSpeed d N) w (PressureStream.streamPotential d (l * a) (l * b) N w f) ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.reconstructedBeta_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (C : E →L[ℝ] F) (M N u : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) (znew : E) (zold : F) (haxial : C znew = l • zold) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) : PressureStream.streamBeta znew (PressureStream.streamPotential d a b M v (pull l C u f)) z = u * PressureStream.streamBeta zold (PressureStream.streamPotential d (l * a) (l * b) N w f) ((chartLinear l C) z)

theorem NavierStokes.MeanChartCompatibility.streamAlias_pull {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (C : E →L[ℝ] F) (M N u : ℝ) (v : E) (w : F) (hshift : M • C v = (N * l ^ d) • w) {f : ℝ × F → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : ℝ × E) (hz : 0 ≤ z.1) : RadialPullback.physicalAlias d a b M v (PressureStream.weightedSource (pull l C u f)) z / z.1 = u * (RadialPullback.physicalAlias d (l * a) (l * b) N w (PressureStream.weightedSource f) ((chartLinear l C) z) / (l * z.1))

The axial alias itself transforms as a velocity. It is retained as the exact compactification term.

theorem NavierStokes.MeanChartCompatibility.pressureAlias_eq_source_sub_derivative {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : TorusInverse.Plane) {f : PressureStream.Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : PressureStream.Lift S) : PressureStream.pressureAlias d a b M hab v f z = PressureStream.pressureSource a b hab f z - PressureStream.graphDr (PressureStream.physicalSpeed d M) (0, v) (PressureStream.meanPressure d a b M hab v f) z

theorem NavierStokes.MeanChartCompatibility.pressureAlias_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l a b d : ℝ} (hl : 0 < l) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (P : S →L[ℝ] T) (k : ℕ) (M N u : ℝ) (v w : TorusInverse.Plane) (hshift : M • (TemporalMeanUpdate.coverMap k) v = (N * l ^ d) • w) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (hs : RadialAlias.RadiallySupported (l * a) (l * b) f) (z : PressureStream.Lift S) (hz : 0 ≤ z.1) : PressureStream.pressureAlias d a b M hab v (coverPull l P k u f) z = coverPull l P k u (PressureStream.pressureAlias d (l * a) (l * b) N ⋯ w f) z

noncomputable def NavierStokes.MeanChartCompatibility.commonTemporalPotential {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) : PressureStream.Lift S → ℝ

The potential uses the explicitly chosen common torus index.

Equations

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

noncomputable def NavierStokes.MeanChartCompatibility.commonTemporalFields {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (epsilon : ℕ → ℝ) (axial : S × TorusInverse.Plane) (fθ fz : ℕ → PressureStream.Lift S → ℝ) : MeanIncrementBounds.Triple (PressureStream.Lift S)

Common temporal fields, bundling radial, angular, axial.

Equations

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

noncomputable def NavierStokes.MeanChartCompatibility.commonTemporalAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) : PressureStream.Lift S → ℝ

Common temporal alias, constructed using PressureStream.divideRadius.

Equations

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

noncomputable def NavierStokes.MeanChartCompatibility.commonTemporalIncrement {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (axial : S × TorusInverse.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : MeanIncrementBounds.Triple (PressureStream.Lift S)

Common temporal increment, given by commonTemporalFields r h index c.operators.epsilon axial (u.thetaResidual c) (u.axialResidual c).

Equations

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

theorem NavierStokes.MeanChartCompatibility.commonTemporalIncrement_native {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (r : CorrectionState.ReconstructionData) (h : ℝ) (axial : S × TorusInverse.Plane) (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) : commonTemporalIncrement (fun (x : ℕ) => r) h (ChartScales.nativeIndex h) axial c u = CorrectionState.temporalIncrement r h axial c u

theorem NavierStokes.MeanChartCompatibility.commonTemporalPotential_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) (ha : 0 < (r n).inner) (hd : 0 < (r n).exponent) (hf : ContDiff ℝ (↑⊤) (f n)) (hp : PressureStream.TorusPeriodicLift (f n)) (hs : RadialAlias.RadiallySupported (r n).inner (r n).outer (f n)) : ContDiff ℝ (↑⊤) (commonTemporalPotential r h index f n)

theorem NavierStokes.MeanChartCompatibility.commonTemporalPotential_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) (ha : 0 < (r n).inner) (hd : 0 < (r n).exponent) (hf : ContDiff ℝ (↑⊤) (f n)) (hp : PressureStream.TorusPeriodicLift (f n)) (hs : RadialAlias.RadiallySupported (r n).inner (r n).outer (f n)) : RadialAlias.RadiallySupported (r n).inner (r n).outer (commonTemporalPotential r h index f n)

theorem NavierStokes.MeanChartCompatibility.commonTemporalAlias_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (f : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) (ha : 0 < (r n).inner) (hd : 0 < (r n).exponent) (hf : ContDiff ℝ (↑⊤) (f n)) (hp : PressureStream.TorusPeriodicLift (f n)) (hs : RadialAlias.RadiallySupported (r n).inner (r n).outer (f n)) : ContDiff ℝ (↑⊤) (commonTemporalAlias r h index f n)

theorem NavierStokes.MeanChartCompatibility.commonTemporalFields_axial_eq {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (epsilon : ℕ → ℝ) (axial : S × TorusInverse.Plane) (fθ fz : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) (ha : 0 < (r n).inner) (hd : 0 < (r n).exponent) (hf : ContDiff ℝ (↑⊤) (fz n)) (hp : PressureStream.TorusPeriodicLift (fz n)) (hs : RadialAlias.RadiallySupported (r n).inner (r n).outer (fz n)) : (commonTemporalFields r h index epsilon axial fθ fz).axial n = fun (z : PressureStream.Lift S) => temporalAtIndex h n (index n) (fz n) z - commonTemporalAlias r h index fz n z

theorem NavierStokes.MeanChartCompatibility.commonTemporalFields_fast_cancellation {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (r : ℕ → CorrectionState.ReconstructionData) (h : ℝ) (index : ℕ → ℕ) (epsilon : ℕ → ℝ) (axial : S × TorusInverse.Plane) (fθ fz : ℕ → PressureStream.Lift S → ℝ) (n : ℕ) (ha : 0 < (r n).inner) (hd : 0 < (r n).exponent) (hθ : ContDiff ℝ (↑⊤) (fθ n)) (hz : ContDiff ℝ (↑⊤) (fz n)) (hpθ : PressureStream.TorusPeriodicLift (fθ n)) (hpz : PressureStream.TorusPeriodicLift (fz n)) (hsz : RadialAlias.RadiallySupported (r n).inner (r n).outer (fz n)) (z : PressureStream.Lift S) : fastAtIndex h n (index n) ((commonTemporalFields r h index epsilon axial fθ fz).angular n) z + TemporalMeanUpdate.centered (fθ n) z = 0 ∧ fastAtIndex h n (index n) ((commonTemporalFields r h index epsilon axial fθ fz).axial n) z + TemporalMeanUpdate.centered (fz n) z = -fastAtIndex h n (index n) (commonTemporalAlias r h index fz n) z

noncomputable def NavierStokes.MeanChartCompatibility.physicalAuxiliary (h : ℝ) (n i : ℕ) : TorusInverse.Plane × TorusInverse.Plane →L[ℝ] TorusInverse.Plane × TorusInverse.Plane

Physical auxiliary, given by (slowToChart h n).prodMap (TemporalMeanUpdate.coverMap i).

Equations

• NavierStokes.MeanChartCompatibility.physicalAuxiliary h n i = (NavierStokes.MeanChartCompatibility.slowToChart h n).prodMap (NavierStokes.TemporalMeanUpdate.coverMap i)

noncomputable def NavierStokes.MeanChartCompatibility.axialUnit : TorusInverse.Plane × TorusInverse.Plane

Axial unit, given by ((1, 0), (0, 0)).

Equations

• NavierStokes.MeanChartCompatibility.axialUnit = ((1, 0), 0, 0)

theorem NavierStokes.MeanChartCompatibility.physicalAuxiliary_radial (h : ℝ) (n i : ℕ) (d M : ℝ) : M • (physicalAuxiliary h n i) (0, TorusInverse.vector TorusInverse.Direction.radial) = (radialFrequency h n i d M * chartScale n ^ d) • (0, TorusInverse.vector TorusInverse.Direction.radial)

theorem NavierStokes.MeanChartCompatibility.physicalAuxiliary_temporal (h : ℝ) (n i : ℕ) : (physicalAuxiliary h n i) (0, TorusInverse.vector TorusInverse.Direction.temporal) = ChartScales.Tg ^ i • (0, TorusInverse.vector TorusInverse.Direction.temporal)

theorem NavierStokes.MeanChartCompatibility.physicalAuxiliary_axial (h : ℝ) (n i : ℕ) : (physicalAuxiliary h n i) axialUnit = chartScale n • ChartScales.epsilon h n • axialUnit

theorem NavierStokes.MeanChartCompatibility.physicalFast_naturality (h : ℝ) (n i : ℕ) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z : PressureStream.Lift TorusInverse.Plane) : fieldOnPhysical h n i (2 * CoordinateAlgebra.A h + 1 / 2) (fastAtIndex h n i f) z = PressureStream.graphDz (0, TorusInverse.vector TorusInverse.Direction.temporal) (fieldOnPhysical h n i (CoordinateAlgebra.A h) f) z

theorem NavierStokes.MeanChartCompatibility.physicalGamma_naturality {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (h : ℝ) (n i : ℕ) (M : ℝ) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (chartScale n * a) (chartScale n * b) f) (z : PressureStream.Lift TorusInverse.Plane) (hz : 0 ≤ z.1) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, TorusInverse.vector TorusInverse.Direction.radial) (PressureStream.streamPotential d a b M (0, TorusInverse.vector TorusInverse.Direction.radial) (fieldOnPhysical h n i (CoordinateAlgebra.A h) f)) z = fieldOnPhysical h n i (CoordinateAlgebra.A h) (PressureStream.streamGamma (PressureStream.physicalSpeed d (radialFrequency h n i d M)) (0, TorusInverse.vector TorusInverse.Direction.radial) (PressureStream.streamPotential d (chartScale n * a) (chartScale n * b) (radialFrequency h n i d M) (0, TorusInverse.vector TorusInverse.Direction.radial) f)) z

theorem NavierStokes.MeanChartCompatibility.physicalBeta_naturality {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (h : ℝ) (n i : ℕ) (M : ℝ) {f : PressureStream.Lift TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported (chartScale n * a) (chartScale n * b) f) (z : PressureStream.Lift TorusInverse.Plane) : PressureStream.streamBeta axialUnit (PressureStream.streamPotential d a b M (0, TorusInverse.vector TorusInverse.Direction.radial) (fieldOnPhysical h n i (CoordinateAlgebra.A h) f)) z = fieldOnPhysical h n i (CoordinateAlgebra.A h) (PressureStream.streamBeta (ChartScales.epsilon h n • axialUnit) (PressureStream.streamPotential d (chartScale n * a) (chartScale n * b) (radialFrequency h n i d M) (0, TorusInverse.vector TorusInverse.Direction.radial) f)) z

noncomputable def NavierStokes.MeanChartCompatibility.physicalTemporalFields (d a b M : ℝ) (Fθ Fz : PressureStream.Lift TorusInverse.Plane → ℝ) (z : PressureStream.Lift TorusInverse.Plane) : Fin 3 → ℝ

One physical vector field, constructed from the two physical sources.

Equations

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

theorem NavierStokes.MeanChartCompatibility.commonTemporalFields_represents {d a b : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (h M : ℝ) (index : ℕ → ℕ) (fθ fz : ℕ → PressureStream.Lift TorusInverse.Plane → ℝ) (Fθ Fz : PressureStream.Lift TorusInverse.Plane → ℝ) (hθ : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (fθ n)) (hz : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (fz n)) (hpθ : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (fθ n)) (hpz : ∀ (n : ℕ), PressureStream.TorusPeriodicLift (fz n)) (hsz : ∀ (n : ℕ), RadialAlias.RadiallySupported (chartScale n * a) (chartScale n * b) (fz n)) (hsourceθ : ∀ (n : ℕ), fieldOnPhysical h n (index n) (2 * CoordinateAlgebra.A h + 1 / 2) (fθ n) = Fθ) (hsourcez : ∀ (n : ℕ), fieldOnPhysical h n (index n) (2 * CoordinateAlgebra.A h + 1 / 2) (fz n) = Fz) (n : ℕ) (z : PressureStream.Lift TorusInverse.Plane) (hr : 0 ≤ z.1) : have δ := commonTemporalFields (fun (k : ℕ) => bandReconstruction h k (index k) d a b M hab) h index (ChartScales.epsilon h) axialUnit fθ fz; ![fieldOnPhysical h n (index n) (CoordinateAlgebra.A h) (δ.radial n) z, fieldOnPhysical h n (index n) (CoordinateAlgebra.A h) (δ.angular n) z, fieldOnPhysical h n (index n) (CoordinateAlgebra.A h) (δ.axial n) z] = physicalTemporalFields d a b M Fθ Fz z

The three defined chart components are restrictions of one physical vector field. The source identities are the only compatibility premises.

noncomputable def NavierStokes.MeanChartCompatibility.sourceMoment {S : Type} (m : ℕ) (f : PressureStream.Lift S → ℝ) (s : S) : ℝ

Source moment, given by PressureStream.pressureMass (fun z => z.1 ^ m * f z) s.

Equations

• NavierStokes.MeanChartCompatibility.sourceMoment m f s = NavierStokes.PressureStream.pressureMass (fun (z : NavierStokes.PressureStream.Lift S) => z.1 ^ m * f z) s

noncomputable def NavierStokes.MeanChartCompatibility.sourceDebt {S : Type} (g qθ qz : PressureStream.Lift S → ℝ) (s : S) : MeanRankUpdate.Debt

Source debt, given by ![sourceMoment 0 g s, sourceMoment 2 qθ s, sourceMoment 1 qz s - (1 / 2 : ℝ) * sourceMoment 2 g s].

Equations

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

theorem NavierStokes.MeanChartCompatibility.sourceMoment_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S →L[ℝ] T) (k m : ℕ) (u : ℝ) {f : PressureStream.Lift T → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : PressureStream.TorusPeriodicLift f) (s : S) : sourceMoment m (coverPull l P k u f) s = u / l ^ (m + 1) * sourceMoment m f (P s)

theorem NavierStokes.MeanChartCompatibility.sourceDebt_coverPull {S T : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup T] [NormedSpace ℝ T] {l : ℝ} (hl : 0 < l) (P : S →L[ℝ] T) (k : ℕ) (u : ℝ) {g qθ qz : PressureStream.Lift T → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hθ : ContDiff ℝ (↑⊤) qθ) (hz : ContDiff ℝ (↑⊤) qz) (hpg : PressureStream.TorusPeriodicLift g) (hpθ : PressureStream.TorusPeriodicLift qθ) (hpz : PressureStream.TorusPeriodicLift qz) (s : S) : sourceDebt (coverPull l P k (l * u ^ 2) g) (coverPull l P k (u ^ 2) qθ) (coverPull l P k (u ^ 2) qz) s = MeanRankUpdate.scaleDebt l⁻¹ u (sourceDebt g qθ qz (P s))

The radial source carries one additional inverse-length factor. The actual three integrated debts then have the required different length powers.

theorem NavierStokes.MeanChartCompatibility.stateDebt_eq_sourceDebt {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (c : CorrectionState.Context (PressureStream.Lift S)) (u : CorrectionState.State (PressureStream.Lift S)) (n : ℕ) (s : S) : CorrectionState.debt c u n s = sourceDebt (u.gr c n) ((MeanIncrementBounds.thetaAxial c.base u.mean + u.covariance 2 1) n) ((MeanIncrementBounds.axialAxial c.base u.mean + u.covariance 2 2) n) s

theorem NavierStokes.MeanChartCompatibility.rankAngularFamily_transport {S T : Type} {l u : ℝ} (hl : l ≠ 0) (hu : u ≠ 0) (P : S → T) (lam a b : ℝ) (ell U C : S → ℝ) (debt : S → MeanRankUpdate.Debt) (ell' U' C' : T → ℝ) (debt' : T → MeanRankUpdate.Debt) (hell : ∀ (s : S), ell s ≠ 0) (hU : ∀ (s : S), U s ≠ 0) (hlength : ∀ (s : S), ell' (P s) = l * ell s) (hvelocity : ∀ (s : S), U' (P s) = u * U s) (hcoefficient : ∀ (s : S), C' (P s) = C s) (hdebt : ∀ (s : S), debt' (P s) = MeanRankUpdate.scaleDebt l u (debt s)) (r : ℝ) (s : S) : MeanRankUpdate.angularFamily lam a b ell' U' C' debt' (l * r, P s) = u * MeanRankUpdate.angularFamily lam a b ell U C debt (r, s)

Naturality with slow-dependent length, velocity, amplitude and debt. Only the primitive input data are transported.

theorem NavierStokes.MeanChartCompatibility.rankDesiredAxialFamily_transport {S T : Type} {l u : ℝ} (hl : l ≠ 0) (hu : u ≠ 0) (P : S → T) (lam a b : ℝ) (ell U C : S → ℝ) (debt : S → MeanRankUpdate.Debt) (ell' U' C' : T → ℝ) (debt' : T → MeanRankUpdate.Debt) (hell : ∀ (s : S), ell s ≠ 0) (hU : ∀ (s : S), U s ≠ 0) (hlength : ∀ (s : S), ell' (P s) = l * ell s) (hvelocity : ∀ (s : S), U' (P s) = u * U s) (hcoefficient : ∀ (s : S), C' (P s) = C s) (hdebt : ∀ (s : S), debt' (P s) = MeanRankUpdate.scaleDebt l u (debt s)) (r : ℝ) (s : S) : MeanRankUpdate.desiredAxialFamily lam a b ell' U' C' debt' (l * r, P s) = u * MeanRankUpdate.desiredAxialFamily lam a b ell U C debt (r, s)

noncomputable def NavierStokes.MeanChartCompatibility.slowProjection (z : PressureStream.Lift TorusInverse.Plane) : SimilarityHomogeneity.ChartPoint

Slow projection, given by (z.1, z.2.1).

Equations

• NavierStokes.MeanChartCompatibility.slowProjection z = (z.1, z.2.1)

theorem NavierStokes.MeanChartCompatibility.slowProjection_physicalToChart (h : ℝ) (n i : ℕ) (z : PressureStream.Lift TorusInverse.Plane) : slowProjection ((physicalToChart h n i) z) = SimilarityHomogeneity.chartTransition h 1 (ChartScales.Q n) (slowProjection z)

theorem NavierStokes.MeanChartCompatibility.physicalProfile_inner {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n i : ℕ) {z : PressureStream.Lift TorusInverse.Plane} (hz : 0 < z.2.1.2) : SimilarityHomogeneity.chartInner h (slowProjection ((physicalToChart h n i) z)) = SimilarityHomogeneity.chartInner h (slowProjection z)

theorem NavierStokes.MeanChartCompatibility.physicalProfile_weight {V : Type} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n i : ℕ) {z : PressureStream.Lift TorusInverse.Plane} (hz : 0 < z.2.1.2) (w : ℝ × ℝ → V) : w (SimilarityHomogeneity.chartInner h (slowProjection ((physicalToChart h n i) z))) = w (SimilarityHomogeneity.chartInner h (slowProjection z))

Every function of the true profile coordinates (X,η) is invariant, including the radial profile weight and its logarithmic edge distance.

theorem NavierStokes.MeanChartCompatibility.physicalProfile_q {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (n i : ℕ) {z : PressureStream.Lift TorusInverse.Plane} (hz : 0 < z.2.1.2) : SimilarityHomogeneity.chartQ h (slowProjection ((physicalToChart h n i) z)) = (ChartScales.Q n)⁻¹ * SimilarityHomogeneity.chartQ h (slowProjection z)

The slow similarity length itself scales; it is not a fixed radial endpoint shared by all normalized band charts.