Exact radial aliases and Fourier suppression

The compactification defect is retained as an actual function. Its averaging and integration-by-parts identities concern genuine Bochner integrals.

@[reducible, inline]

abbrev NavierStokes.FourierAlias.State : Type

State: an abbreviation for ℝ × Plane.

Equations

• NavierStokes.FourierAlias.State = (ℝ × NavierStokes.TorusInverse.Plane)

noncomputable def NavierStokes.FourierAlias.TorusPeriodic {F : Type} (f : TorusInverse.Plane → F) : Prop

Integer translation invariance of an actual function on the universal cover.

Equations

• NavierStokes.FourierAlias.TorusPeriodic f = ∀ (Y : NavierStokes.TorusInverse.Plane) (k : NavierStokes.TorusInverse.Frequency), f (Y + (↑k.1, ↑k.2)) = f Y

noncomputable def NavierStokes.FourierAlias.torusMean {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : TorusInverse.Plane → F) : F

The actual normalized unit-square average.

Equations

• NavierStokes.FourierAlias.torusMean f = ∫ (y : ℝ) (x : ℝ) in 0..1, f (x, y)

noncomputable def NavierStokes.FourierAlias.sliceMean {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : State → F) (U : ℝ) : F

Slice mean, given by torusMean (fun Y => f (U, Y)).

Equations

• NavierStokes.FourierAlias.sliceMean f U = NavierStokes.FourierAlias.torusMean fun (Y : NavierStokes.TorusInverse.Plane) => f (U, Y)

noncomputable def NavierStokes.FourierAlias.cutoffAlias {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (χ : ℝ → ℝ) (M : ℝ) (v : TorusInverse.Plane) (f : State → F) (z : State) : F

The exact defect in D Ic = f - cutoffAlias.

Equations

• NavierStokes.FourierAlias.cutoffAlias χ M v f z = deriv χ z.1 • NavierStokes.TransportPrimitive.totalIntegral M v f z

theorem NavierStokes.FourierAlias.torusPeriodic_first {F : Type} {f : TorusInverse.Plane → F} (hp : TorusPeriodic f) (y : ℝ) : Function.Periodic (fun (x : ℝ) => f (x, y)) 1

theorem NavierStokes.FourierAlias.torusPeriodic_second {F : Type} {f : TorusInverse.Plane → F} (hp : TorusPeriodic f) (x : ℝ) : Function.Periodic (fun (y : ℝ) => f (x, y)) 1

theorem NavierStokes.FourierAlias.periodic_integral_translate {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : ℝ → F} (hg : Function.Periodic g 1) (c : ℝ) : ∫ (x : ℝ) in 0..1, g (x + c) = ∫ (x : ℝ) in 0..1, g x

theorem NavierStokes.FourierAlias.torusMean_translate {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : TorusInverse.Plane → F} (hp : TorusPeriodic f) (Y : TorusInverse.Plane) : (torusMean fun (Z : TorusInverse.Plane) => f (Z + Y)) = torusMean f

Averaging is invariant under any real torus translation.

theorem NavierStokes.FourierAlias.torusMean_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (f : TorusInverse.Plane → F) : (torusMean fun (Y : TorusInverse.Plane) => c • f Y) = c • torusMean f

theorem NavierStokes.FourierAlias.intervalIntegral_comm {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : TorusInverse.Plane → F} (hg : Continuous g) {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) : ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, g (x, y) = ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, g (x, y)

Fubini on two compact real intervals.

theorem NavierStokes.FourierAlias.continuous_parameter_interval {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type} [TopologicalSpace H] [FirstCountableTopology H] [LocallyCompactSpace H] {g : H × ℝ → F} (hg : Continuous g) {a b : ℝ} (hab : a ≤ b) : Continuous fun (x : H) => ∫ (u : ℝ) in a..b, g (x, u)

theorem NavierStokes.FourierAlias.torusMean_const {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (c : F) : (torusMean fun (x : TorusInverse.Plane) => c) = c

theorem NavierStokes.FourierAlias.torusMean_neg {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : TorusInverse.Plane → F) : (torusMean fun (Y : TorusInverse.Plane) => -f Y) = -torusMean f

theorem NavierStokes.FourierAlias.torusMean_add {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : TorusInverse.Plane → F} (hf : Continuous f) (hg : Continuous g) : (torusMean fun (Y : TorusInverse.Plane) => f Y + g Y) = torusMean f + torusMean g

theorem NavierStokes.FourierAlias.torusMean_sub {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : TorusInverse.Plane → F} (hf : Continuous f) (hg : Continuous g) : (torusMean fun (Y : TorusInverse.Plane) => f Y - g Y) = torusMean f - torusMean g

theorem NavierStokes.FourierAlias.torusMean_intervalIntegral {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : State → F} (hg : Continuous g) {a b : ℝ} (hab : a ≤ b) : (torusMean fun (Y : TorusInverse.Plane) => ∫ (s : ℝ) in a..b, g (s, Y)) = ∫ (s : ℝ) in a..b, sliceMean g s

The torus and radial averages commute as actual iterated integrals.

theorem NavierStokes.FourierAlias.torusMean_totalIntegral {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} (hab : a ≤ b) (hf : Continuous f) (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (hs : RadialAlias.RadiallySupported a b f) (U : ℝ) : sliceMean (TransportPrimitive.totalIntegral M v f) U = ∫ (s : ℝ) in a..b, sliceMean f s

The shifted total integral has exactly the radially integrated source mean.

theorem NavierStokes.FourierAlias.totalIntegral_periodic {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {M : ℝ} {v : TorusInverse.Plane} {f : State → F} (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (U : ℝ) : TorusPeriodic fun (Y : TorusInverse.Plane) => TransportPrimitive.totalIntegral M v f (U, Y)

theorem NavierStokes.FourierAlias.cutoffAlias_periodic {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : ℝ → ℝ} {M : ℝ} {v : TorusInverse.Plane} {f : State → F} (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (U : ℝ) : TorusPeriodic fun (Y : TorusInverse.Plane) => cutoffAlias χ M v f (U, Y)

theorem NavierStokes.FourierAlias.cutoffAlias_supported_on_transition {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {c d M : ℝ} {v : TorusInverse.Plane} {f : State → F} {χ : ℝ → ℝ} (hleft : ∀ u ≤ c, χ u = 0) (hright : ∀ (u : ℝ), d ≤ u → χ u = 1) : RadialAlias.RadiallySupported c d (cutoffAlias χ M v f)

The exact defect is supported in the transition interval of the cutoff, which may be strictly inside the radial support interval of the source.

theorem NavierStokes.FourierAlias.cutoffAlias_zero_mean_of_integratedMean_zero {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} (χ : ℝ → ℝ) (hab : a ≤ b) (hf : Continuous f) (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (hs : RadialAlias.RadiallySupported a b f) (hm : ∫ (s : ℝ) in a..b, sliceMean f s = 0) (U : ℝ) : sliceMean (cutoffAlias χ M v f) U = 0

theorem NavierStokes.FourierAlias.cutoffAlias_zero_mean {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} (χ : ℝ → ℝ) (hab : a ≤ b) (hf : Continuous f) (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (U : ℝ), sliceMean f U = 0) (U : ℝ) : sliceMean (cutoffAlias χ M v f) U = 0

theorem NavierStokes.FourierAlias.transport_compact_eq_sub_alias {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : State) : TransportPrimitive.fixedDeriv (1, M • v) (TransportPrimitive.compactIntegral χ M v f) z = f z - cutoffAlias χ M v f z

The alias is an exact term in the constructed inverse identity.

theorem NavierStokes.FourierAlias.iteratedFDeriv_periodic {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : State → F} (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (n : ℕ) (U : ℝ) : TorusPeriodic fun (Y : TorusInverse.Plane) => iteratedFDeriv ℝ n f (U, Y)

theorem NavierStokes.FourierAlias.periodic_finiteJet_bound {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : State → F} (hf : ContDiff ℝ (↑⊤) f) (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (a b : ℝ) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ j ≤ m, ∀ U ∈ Set.Icc a b, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j f (U, Y)‖ ≤ C

Actual smooth periodic fields have bounded finite prefixes of full Fréchet jets on every compact radial slab.

theorem NavierStokes.FourierAlias.cutoffAlias_smooth {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (cutoffAlias χ M v f)

theorem NavierStokes.FourierAlias.cutoffAlias_supported {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : TorusInverse.Plane} {f : State → F} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) : RadialAlias.RadiallySupported a b (cutoffAlias χ M v f)

theorem NavierStokes.FourierAlias.cutoffAlias_finiteJet_bound {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {f : State → F} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ∀ (U : ℝ), TorusPeriodic fun (Y : TorusInverse.Plane) => f (U, Y)) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ℝ) (v : TorusInverse.Plane), ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ M v f) z‖ ≤ C

Before using oscillation, every finite prefix of alias jets has a bound uniform in both the frequency and the translation direction.

theorem NavierStokes.FourierAlias.sourceJet_smooth (J : (State → ℂ) → State → ℂ) (f : State → ℂ) (p : ℕ) (hf : ContDiff ℝ (↑⊤) f) (hJ : ∀ n < p, ContDiff ℝ (↑⊤) (J (RadialAlias.sourceJet J f n))) : ContDiff ℝ (↑⊤) (RadialAlias.sourceJet J f p)

theorem NavierStokes.FourierAlias.totalIntegral_sourceJet {a b M : ℝ} {v : TorusInverse.Plane} (J : (State → ℂ) → State → ℂ) (f : State → ℂ) (p : ℕ) (hM : M ≠ 0) (hf : ContDiff ℝ (↑⊤) f) (hsf : RadialAlias.RadiallySupported a b f) (hJ : ∀ n < p, ContDiff ℝ (↑⊤) (J (RadialAlias.sourceJet J f n))) (hsJ : ∀ n < p, RadialAlias.RadiallySupported a b (J (RadialAlias.sourceJet J f n))) (hr : ∀ n < p, RadialAlias.directionalDeriv v (J (RadialAlias.sourceJet J f n)) = RadialAlias.sourceJet J f n) (z : State) : TransportPrimitive.totalIntegral M v f z = (-M⁻¹) ^ p • TransportPrimitive.totalIntegral M v (RadialAlias.sourceJet J f p) z

The existing repeated IBP identity, now for the actual U-dependent total integral. No alias is discarded.

theorem NavierStokes.FourierAlias.cutoffAlias_sourceJet {a b M : ℝ} {v : TorusInverse.Plane} (χ : ℝ → ℝ) (J : (State → ℂ) → State → ℂ) (f : State → ℂ) (p : ℕ) (hM : M ≠ 0) (hf : ContDiff ℝ (↑⊤) f) (hsf : RadialAlias.RadiallySupported a b f) (hJ : ∀ n < p, ContDiff ℝ (↑⊤) (J (RadialAlias.sourceJet J f n))) (hsJ : ∀ n < p, RadialAlias.RadiallySupported a b (J (RadialAlias.sourceJet J f n))) (hr : ∀ n < p, RadialAlias.directionalDeriv v (J (RadialAlias.sourceJet J f n)) = RadialAlias.sourceJet J f n) (z : State) : cutoffAlias χ M v f z = (-M⁻¹) ^ p • cutoffAlias χ M v (RadialAlias.sourceJet J f p) z

theorem NavierStokes.FourierAlias.iteratedFDeriv_cutoffAlias_sourceJet {a b M : ℝ} {v : TorusInverse.Plane} {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (J : (State → ℂ) → State → ℂ) (f : State → ℂ) (p : ℕ) (hM : M ≠ 0) (hf : ContDiff ℝ (↑⊤) f) (hsf : RadialAlias.RadiallySupported a b f) (hJ : ∀ n < p, ContDiff ℝ (↑⊤) (J (RadialAlias.sourceJet J f n))) (hsJ : ∀ n < p, RadialAlias.RadiallySupported a b (J (RadialAlias.sourceJet J f n))) (hr : ∀ n < p, RadialAlias.directionalDeriv v (J (RadialAlias.sourceJet J f n)) = RadialAlias.sourceJet J f n) (m : ℕ) (z : State) : iteratedFDeriv ℝ m (cutoffAlias χ M v f) z = (-M⁻¹) ^ p • iteratedFDeriv ℝ m (cutoffAlias χ M v (RadialAlias.sourceJet J f p)) z

Differentiate the exact scalar IBP identity. This controls full derivative tensors, including every ordinary mixed coordinate derivative.

noncomputable def NavierStokes.FourierAlias.nonbarPart (f : State → ℂ) (z : State) : ℂ

Remove the actual full torus mean at each fixed radial coordinate.

Equations

• NavierStokes.FourierAlias.nonbarPart f z = f z - NavierStokes.ParametricTorusInverse.mean f z.1

theorem NavierStokes.FourierAlias.nonbarPart_smooth {f : State → ℂ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (nonbarPart f)

theorem NavierStokes.FourierAlias.nonbarPart_periodic {f : State → ℂ} (hp : ParametricTorusInverse.Periodic f) : ParametricTorusInverse.Periodic (nonbarPart f)

theorem NavierStokes.FourierAlias.nonbarPart_zeroMean {f : State → ℂ} (hf : ContDiff ℝ (↑⊤) f) : ParametricTorusInverse.ZeroMean (nonbarPart f)

theorem NavierStokes.FourierAlias.nonbarPart_radiallySupported {a b : ℝ} {f : State → ℂ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (nonbarPart f)

theorem NavierStokes.FourierAlias.totalIntegral_nonbarPart {a b M : ℝ} {v : TorusInverse.Plane} {f : State → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∫ (U : ℝ) in a..b, sliceMean f U = 0) (z : State) : TransportPrimitive.totalIntegral M v (nonbarPart f) z = TransportPrimitive.totalIntegral M v f z

theorem NavierStokes.FourierAlias.cutoffAlias_eq_nonbarPart {a b M : ℝ} {v : TorusInverse.Plane} {f : State → ℂ} (χ : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∫ (U : ℝ) in a..b, sliceMean f U = 0) : cutoffAlias χ M v f = cutoffAlias χ M v (nonbarPart f)

If the integrated bar vanishes, subtracting the bar does not change the alias at all. This is the exact reduction used for the pressure source.

noncomputable def NavierStokes.FourierAlias.fourierSourceJet (d : TorusInverse.Direction) (f : State → ℂ) (p : ℕ) : State → ℂ

The successive slow derivatives of actual directional Fourier inverses.

Equations

• NavierStokes.FourierAlias.fourierSourceJet d f p = NavierStokes.RadialAlias.sourceJet (NavierStokes.ParametricTorusInverse.inverse d) f p

theorem NavierStokes.FourierAlias.fourierSourceJet_eq_parameterJet (d : TorusInverse.Direction) {f : State → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (p : ℕ) : fourierSourceJet d f p = ParametricTorusInverse.parameterJet p (ParametricTorusInverse.iterateInverse d p f)

The interleaved construction is exactly the manuscript's slow derivative of the iterated Fourier inverse, because the actual operators commute.

theorem NavierStokes.FourierAlias.inverse_radiallySupported (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (ParametricTorusInverse.inverse d f)

theorem NavierStokes.FourierAlias.fourierSourceJet_properties (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (p : ℕ) : ContDiff ℝ (↑⊤) (fourierSourceJet d f p) ∧ ParametricTorusInverse.Periodic (fourierSourceJet d f p) ∧ ParametricTorusInverse.ZeroMean (fourierSourceJet d f p) ∧ RadialAlias.RadiallySupported a b (fourierSourceJet d f p)

theorem NavierStokes.FourierAlias.cutoffAlias_fourierSourceJet (d : TorusInverse.Direction) {a b M : ℝ} {f : State → ℂ} (χ : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (p : ℕ) (hM : M ≠ 0) (z : State) : cutoffAlias χ M (TorusInverse.vector d) f z = (-M⁻¹) ^ p • cutoffAlias χ M (TorusInverse.vector d) (fourierSourceJet d f p) z

Exact arbitrary-order IBP with the Fourier inverse constructed from the given source's own coefficients. No antiderivative or decay premise remains.

theorem NavierStokes.FourierAlias.cutoffAlias_arbitrary_order (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m p : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ M (TorusInverse.vector d) f) z‖ ≤ C * |M|⁻¹ ^ p

All fixed jets of the exact alias gain arbitrarily many inverse powers of the frequency. The constant precedes the frequency, point, and jet index.

theorem NavierStokes.FourierAlias.cutoffAlias_arbitrary_order_of_integratedMean_zero (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∫ (U : ℝ) in a..b, sliceMean f U = 0) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m p : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ M (TorusInverse.vector d) f) z‖ ≤ C * |M|⁻¹ ^ p

theorem NavierStokes.FourierAlias.torusMean_eq_haar {f : TorusInverse.Plane → ℂ} (hf : Continuous f) (hp : TorusPeriodic f) : torusMean f = ∫ (z : TorusInverse.Torus), (SmoothFourierData.descendContinuous f hf hp) z ∂TorusInverse.torusMeasure

The square average is the normalized Haar average of the actual descent.

theorem NavierStokes.FourierAlias.cutoffAlias_haar_zero (d : TorusInverse.Direction) {a b M : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (U : ℝ) : ∫ (z : TorusInverse.Torus), (SmoothFourierData.descendContinuous (fun (Y : TorusInverse.Plane) => cutoffAlias χ M (TorusInverse.vector d) f (U, Y)) ⋯ ⋯) z ∂TorusInverse.torusMeasure = 0

theorem NavierStokes.FourierAlias.inverse_frequency_eventually_small {M : ℕ → ℝ} {h κ A growth : ℝ} (hh : 0 < h) (hκ : 0 < κ) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ≤ A * ChartScales.epsilon h n ^ κ * ChartScales.S n ^ growth) : ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ≤ ChartScales.epsilon h n ^ (κ / 2)

The actual chart slow scale is subpower relative to epsilon. Consequently an arbitrary fixed slow loss can be absorbed into half of a positive epsilon gain. The reciprocal-frequency premise alone would not imply this for an unrestricted scale S.

theorem NavierStokes.FourierAlias.inverse_frequency_power_le_epsilon {M : ℕ → ℝ} {h κ A growth : ℝ} (hh : 0 < h) (hκ : 0 < κ) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ≤ A * ChartScales.epsilon h n ^ κ * ChartScales.S n ^ growth) (N : ℕ) : ∃ (p : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ^ p ≤ ChartScales.epsilon h n ^ N

For each requested epsilon power one fixed finite IBP order suffices.

theorem NavierStokes.FourierAlias.cutoffAlias_superflat (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {M : ℕ → ℝ} {h κ A growth : ℝ} (hh : 0 < h) (hκ : 0 < κ) (hM : ∀ᶠ (n : ℕ) in Filter.atTop, M n ≠ 0) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ≤ A * ChartScales.epsilon h n ^ κ * ChartScales.S n ^ growth) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ (M n) (TorusInverse.vector d) f) z‖ ≤ C * ChartScales.epsilon h n ^ N

Uniform full-jet superflatness of the retained exact alias. Constants and the eventual threshold may depend on the requested jet order and epsilon power, but not on the frequency index, evaluation point, or smaller jet.

theorem NavierStokes.FourierAlias.cutoffAlias_superflat_of_integratedMean_zero (d : TorusInverse.Direction) {a b : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∫ (U : ℝ) in a..b, sliceMean f U = 0) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {M : ℕ → ℝ} {h κ A growth : ℝ} (hh : 0 < h) (hκ : 0 < κ) (hM : ∀ᶠ (n : ℕ) in Filter.atTop, M n ≠ 0) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, |M n|⁻¹ ≤ A * ChartScales.epsilon h n ^ κ * ChartScales.S n ^ growth) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ (M n) (TorusInverse.vector d) f) z‖ ≤ C * ChartScales.epsilon h n ^ N

theorem NavierStokes.FourierAlias.radial_cutoffAlias_superflat {a b : ℝ} {f : State → ℂ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hp : ParametricTorusInverse.Periodic f) (hm : ParametricTorusInverse.ZeroMean f) (hs : RadialAlias.RadiallySupported a b f) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {h : ℝ} (hh : 0 < h) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : State), ‖iteratedFDeriv ℝ j (cutoffAlias χ (ChartScales.radialCoefficient h n) (TorusInverse.vector TorusInverse.Direction.radial) f) z‖ ≤ C * ChartScales.epsilon h n ^ N

Specialization to the manuscript's explicitly constructed radial frequency, whose reciprocal bound is already proved in ChartScales.