Uniform seminorm bounds for families of exact Fourier aliases

All constants are chosen before the source and the band. The estimates use actual derivatives and actual translated integrals.

Actual torus inversion for smooth finite-dimensional parameter families

The source is an actual jointly smooth function. Fourier coefficients are the unit-square integrals of that source. No output regularity or decay assumptions are part of the construction.

@[reducible, inline]

abbrev NavierStokes.SmoothFamilyTorusInverse.Point (P : Type) : Type

Point: an abbreviation for P × Plane.

Equations

• NavierStokes.SmoothFamilyTorusInverse.Point P = (P × NavierStokes.TorusInverse.Plane)

@[reducible, inline]

abbrev NavierStokes.SmoothFamilyTorusInverse.Source (P : Type) : Type

Source: an abbreviation for Point P → ℂ.

Equations

• NavierStokes.SmoothFamilyTorusInverse.Source P = (NavierStokes.SmoothFamilyTorusInverse.Point P → ℂ)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.slice {P : Type} (f : Source P) (p : P) : TorusInverse.Plane → ℂ

Slice, defined pointwise by f (p, Y).

Equations

• NavierStokes.SmoothFamilyTorusInverse.slice f p Y = f (p, Y)

def NavierStokes.SmoothFamilyTorusInverse.Periodic {P : Type} (f : Source P) : Prop

Periodic, given by ∀ p, SmoothFourierData.UnitPeriodic (slice f p).

Equations

• NavierStokes.SmoothFamilyTorusInverse.Periodic f = ∀ (p : P), NavierStokes.SmoothFourierData.UnitPeriodic (NavierStokes.SmoothFamilyTorusInverse.slice f p)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.coefficient {P : Type} (f : Source P) (p : P) (k : TorusInverse.Frequency) : ℂ

Coefficient, given by SmoothFourierData.coefficient (slice f p) k.

Equations

• NavierStokes.SmoothFamilyTorusInverse.coefficient f p k = NavierStokes.SmoothFourierData.coefficient (NavierStokes.SmoothFamilyTorusInverse.slice f p) k

noncomputable def NavierStokes.SmoothFamilyTorusInverse.mean {P : Type} (f : Source P) (p : P) : ℂ

Mean, given by coefficient f p 0.

Equations

• NavierStokes.SmoothFamilyTorusInverse.mean f p = NavierStokes.SmoothFamilyTorusInverse.coefficient f p 0

def NavierStokes.SmoothFamilyTorusInverse.ZeroMean {P : Type} (f : Source P) : Prop

Zero mean, given by ∀ p, mean f p = 0.

Equations

• NavierStokes.SmoothFamilyTorusInverse.ZeroMean f = ∀ (p : P), NavierStokes.SmoothFamilyTorusInverse.mean f p = 0

noncomputable def NavierStokes.SmoothFamilyTorusInverse.inverse {P : Type} (d : TorusInverse.Direction) (f : Source P) (z : Point P) : ℂ

Inverse, given by directionalInverse d (coefficient f z.1) z.2.

Equations

• NavierStokes.SmoothFamilyTorusInverse.inverse d f z = NavierStokes.TorusInverse.directionalInverse d (NavierStokes.SmoothFamilyTorusInverse.coefficient f z.1) z.2

noncomputable def NavierStokes.SmoothFamilyTorusInverse.fixedPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : Point P) (f : Source P) (z : Point P) : ℂ

Fixed partial, given by fderiv ℝ f z v.

Equations

• NavierStokes.SmoothFamilyTorusInverse.fixedPartial v f z = (fderiv ℝ f z) v

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (v : P) (f : Source P) : Source P

Parameter partial, given by fixedPartial (v, 0) f.

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterPartial v f = NavierStokes.SmoothFamilyTorusInverse.fixedPartial (v, 0) f

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterDerivative {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : Source P) (z : Point P) : P →L[ℝ] ℂ

Parameter derivative, given by (fderiv ℝ f z).comp (ContinuousLinearMap.inl ℝ P Plane).

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterDerivative f z = fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ P NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.SmoothFamilyTorusInverse.torusXJet {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (n : ℕ) (f : Source P) : Source P

Torus X jet, given by (fixedPartial (0, (1, 0)))^[n] f.

Equations

• NavierStokes.SmoothFamilyTorusInverse.torusXJet n f = (NavierStokes.SmoothFamilyTorusInverse.fixedPartial (0, 1, 0))^[n] f

noncomputable def NavierStokes.SmoothFamilyTorusInverse.swapTorus {P : Type} (f : Source P) : Source P

Swap torus, defined pointwise by f (z.1, (z.2.2, z.2.1)).

Equations

• NavierStokes.SmoothFamilyTorusInverse.swapTorus f z = f (z.1, z.2.2, z.2.1)

theorem NavierStokes.SmoothFamilyTorusInverse.slice_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (p : P) : ContDiff ℝ (↑⊤) (slice f p)

theorem NavierStokes.SmoothFamilyTorusInverse.fixedPartial_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (v : Point P) : ContDiff ℝ (↑⊤) (fixedPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (v : P) : ContDiff ℝ (↑⊤) (parameterPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterDerivative_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (parameterDerivative f)

theorem NavierStokes.SmoothFamilyTorusInverse.fixedPartial_periodic {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hp : Periodic f) (v : Point P) : Periodic (fixedPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_periodic {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hp : Periodic f) (v : P) : Periodic (parameterPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.torusXJet_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (torusXJet n f)

theorem NavierStokes.SmoothFamilyTorusInverse.swapTorus_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (swapTorus f)

theorem NavierStokes.SmoothFamilyTorusInverse.slice_hasFDerivAt {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (p : P) (Y : TorusInverse.Plane) : HasFDerivAt (slice f p) (fderiv ℝ f (p, Y) ∘SL ContinuousLinearMap.inr ℝ P TorusInverse.Plane) Y

theorem NavierStokes.SmoothFamilyTorusInverse.parameter_hasFDerivAt {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (p : P) (Y : TorusInverse.Plane) : HasFDerivAt (fun (q : P) => f (q, Y)) (parameterDerivative f (p, Y)) p

theorem NavierStokes.SmoothFamilyTorusInverse.slice_torusXJet {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (p : P) : slice (torusXJet n f) p = SmoothFourierData.xJet n (slice f p)

theorem NavierStokes.SmoothFamilyTorusInverse.mean_eq_integral {P : Type} (f : Source P) (p : P) : mean f p = ∫ (y : ℝ) (x : ℝ) in 0..1, f (p, x, y)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.weightedSource {P : Type} (k : TorusInverse.Frequency) (f : Source P) (q : (P × ℝ) × ℝ) : ℂ

Weighted source, given by SmoothFourierData.kernel k (q.2, q.1.2) * f (q.1.1, (q.2, q.1.2)).

Equations

• NavierStokes.SmoothFamilyTorusInverse.weightedSource k f q = NavierStokes.SmoothFourierData.kernel k (q.2, q.1.2) * f (q.1.1, q.2, q.1.2)

theorem NavierStokes.SmoothFamilyTorusInverse.weightedSource_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (weightedSource k f)

theorem NavierStokes.SmoothFamilyTorusInverse.coefficient_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) : ContDiff ℝ ↑⊤ fun (p : P) => coefficient f p k

noncomputable def NavierStokes.SmoothFamilyTorusInverse.lineSource {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : Source P) (p v : P) : ParametricTorusInverse.Source

Restricting the actual family to a line only changes its external parameter. It leaves every torus Fourier integral unchanged.

Equations

• NavierStokes.SmoothFamilyTorusInverse.lineSource f p v z = f (p + z.1 • v, z.2)

theorem NavierStokes.SmoothFamilyTorusInverse.lineSource_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (p v : P) : ContDiff ℝ (↑⊤) (lineSource f p v)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_lineSource {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (p v : P) : ParametricTorusInverse.parameterPartial (lineSource f p v) = lineSource (parameterPartial v f) p v

theorem NavierStokes.SmoothFamilyTorusInverse.coefficient_fderiv_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) (p v : P) : (fderiv ℝ (fun (q : P) => coefficient f q k) p) v = coefficient (parameterPartial v f) p k

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_zeroMean {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hm : ZeroMean f) (v : P) : ZeroMean (parameterPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.exists_uniform_coefficient_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n : ℕ) {K : Set P} (hK : IsCompact K) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ K, ∀ (k : TorusInverse.Frequency), TorusInverse.weight k ^ n * ‖coefficient f p k‖ ≤ C

noncomputable def NavierStokes.SmoothFamilyTorusInverse.applyMultiplier {P : Type} (m : TorusInverse.Frequency → ℂ) (f : Source P) (z : Point P) : ℂ

Apply multiplier, given by series (fun k => m k * coefficient f z.1 k) z.2.

Equations

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

theorem NavierStokes.SmoothFamilyTorusInverse.multiplied_coeff_rapid {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (p : P) : TorusInverse.Rapid fun (k : TorusInverse.Frequency) => m k * coefficient f p k

theorem NavierStokes.SmoothFamilyTorusInverse.uniform_multiplied_coeff_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) {K : Set P} (hK : IsCompact K) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ K, ∀ (k : TorusInverse.Frequency), ‖m k * coefficient f p k‖ ≤ C * (TorusInverse.weight k ^ 4)⁻¹

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_partial {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (v : E) (n : ℕ) (z : E) : ‖iteratedFDeriv ℝ n (fun (x : E) => (fderiv ℝ f x) v) z‖ ≤ ‖v‖ * ‖iteratedFDeriv ℝ (n + 1) f z‖

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_linear {E F G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (z : E) : ‖iteratedFDeriv ℝ n (fun (x : E) => L (f x)) z‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ n f z‖

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_add {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : E → F} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (z : E) : ‖iteratedFDeriv ℝ n (fun (x : E) => f x + g x) z‖ ≤ ‖iteratedFDeriv ℝ n f z‖ + ‖iteratedFDeriv ℝ n g z‖

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_sum {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type} [Fintype ι] {f : ι → E → F} (hf : ∀ (i : ι), ContDiff ℝ (↑⊤) (f i)) (n : ℕ) (z : E) : ‖iteratedFDeriv ℝ n (fun (x : E) => ∑ i : ι, f i x) z‖ ≤ ∑ i : ι, ‖iteratedFDeriv ℝ n (f i) z‖

noncomputable def NavierStokes.SmoothFamilyTorusInverse.repeatPartial {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (v : E) (n : ℕ) (f : E → F) : E → F

Repeat partial, given by (fun g x => fderiv ℝ g x v)^[n] f.

Equations

• NavierStokes.SmoothFamilyTorusInverse.repeatPartial v n f = (fun (g : E → F) (x : E) => (fderiv ℝ g x) v)^[n] f

theorem NavierStokes.SmoothFamilyTorusInverse.norm_repeatPartial {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) (v : E) (n : ℕ) (z : E) : ‖repeatPartial v n f z‖ ≤ ‖v‖ ^ n * ‖iteratedFDeriv ℝ n f z‖

noncomputable def NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord {G : Type} [NormedAddCommGroup G] [NormedSpace ℝ G] : List Bool → (TorusInverse.Plane → G) → TorusInverse.Plane → G

Tensor torus word as an element of w, g => fun Y => fderiv ℝ (tensorTorusWord w g) Y (if b then (0, 1) else (1, 0)).

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord [] x✝ = x✝

theorem NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord_smooth {G : Type} [NormedAddCommGroup G] [NormedSpace ℝ G] {g : TorusInverse.Plane → G} (hg : ContDiff ℝ (↑⊤) g) (w : List Bool) : ContDiff ℝ (↑⊤) (tensorTorusWord w g)

theorem NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord_map {G H : Type} [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] (L : G →L[ℝ] H) {g : TorusInverse.Plane → G} (hg : ContDiff ℝ (↑⊤) g) (w : List Bool) : (tensorTorusWord w fun (Y : TorusInverse.Plane) => L (g Y)) = fun (Y : TorusInverse.Plane) => L (tensorTorusWord w g Y)

theorem NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord_scalar (g : TorusInverse.Plane → ℂ) (w : List Bool) : tensorTorusWord w g = TorusInverse.derivativeWord w g

theorem NavierStokes.SmoothFamilyTorusInverse.tensorTorusWord_replicate (g : TorusInverse.Plane → ℂ) (n : ℕ) : tensorTorusWord (List.replicate n false) g = SmoothFourierData.xJet n g

@[reducible, inline]

abbrev NavierStokes.SmoothFamilyTorusInverse.BasisIndex (P : Type) [NormedAddCommGroup P] [NormedSpace ℝ P] : Type

Basis index: an abbreviation for Fin (Module.finrank ℝ P).

Equations

• NavierStokes.SmoothFamilyTorusInverse.BasisIndex P = Fin (Module.finrank ℝ P)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterBasis {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] : Module.Basis (BasisIndex P) ℝ P

Parameter basis, given by Module.finBasis ℝ P.

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterBasis = Module.finBasis ℝ P

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterCoord {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (i : BasisIndex P) : P →L[ℝ] ℝ

Parameter coord, given by ((parameterBasis (P := P)).coord i).toContinuousLinearMap.

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterCoord i = LinearMap.toContinuousLinearMap (NavierStokes.SmoothFamilyTorusInverse.parameterBasis.coord i)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterLift {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (i : BasisIndex P) : ℂ →L[ℝ] Point P →L[ℝ] ℂ

Parameter lift, given by ContinuousLinearMap.smulRightL ℝ (Point P) ℂ ((parameterCoord i).comp (ContinuousLinearMap.fst ℝ P Plane)).

Equations

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

noncomputable def NavierStokes.SmoothFamilyTorusInverse.torusLiftX {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : ℂ →L[ℝ] Point P →L[ℝ] ℂ

Torus lift X, given by ContinuousLinearMap.smulRightL ℝ (Point P) ℂ (dx.comp (ContinuousLinearMap.snd ℝ P Plane)).

Equations

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

noncomputable def NavierStokes.SmoothFamilyTorusInverse.torusLiftY {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] : ℂ →L[ℝ] Point P →L[ℝ] ℂ

Torus lift Y, given by ContinuousLinearMap.smulRightL ℝ (Point P) ℂ (dy.comp (ContinuousLinearMap.snd ℝ P Plane)).

Equations

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

@[simp]

theorem NavierStokes.SmoothFamilyTorusInverse.parameterLift_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (i : BasisIndex P) (c : ℂ) (v : Point P) : ((parameterLift i) c) v = (parameterCoord i) v.1 • c

@[simp]

theorem NavierStokes.SmoothFamilyTorusInverse.torusLiftX_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : ℂ) (v : Point P) : (torusLiftX c) v = v.2.1 • c

@[simp]

theorem NavierStokes.SmoothFamilyTorusInverse.torusLiftY_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (c : ℂ) (v : Point P) : (torusLiftY c) v = v.2.2 • c

theorem NavierStokes.SmoothFamilyTorusInverse.clm_parameter_expansion {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (L : P →L[ℝ] ℂ) (v : P) : L v = ∑ i : BasisIndex P, (parameterCoord i) v • L (parameterBasis i)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.multiplierTermDerivative {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (m : TorusInverse.Frequency → ℂ) (f : Source P) (k : TorusInverse.Frequency) (z : Point P) : Point P →L[ℝ] ℂ

Multiplier term derivative as an element of Point P →L[ℝ] ℂ.

Equations

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

theorem NavierStokes.SmoothFamilyTorusInverse.hasFDerivAt_multiplierTerm {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (m : TorusInverse.Frequency → ℂ) (k : TorusInverse.Frequency) (z : Point P) : HasFDerivAt (fun (w : Point P) => m k * coefficient f w.1 k * TorusInverse.mode k w.2) (multiplierTermDerivative m f k z) z

theorem NavierStokes.SmoothFamilyTorusInverse.norm_multiplierTermDerivative_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (m : TorusInverse.Frequency → ℂ) (f : Source P) (k : TorusInverse.Frequency) (z : Point P) : ‖multiplierTermDerivative m f k z‖ ≤ ∑ i : BasisIndex P, ‖parameterLift i‖ * ‖m k * coefficient (parameterPartial (parameterBasis i) f) z.1 k‖ + ‖torusLiftX‖ * ‖ParametricTorusInverse.multiplierX m k * coefficient f z.1 k‖ + ‖torusLiftY‖ * ‖ParametricTorusInverse.multiplierY m k * coefficient f z.1 k‖

theorem NavierStokes.SmoothFamilyTorusInverse.uniform_multiplierDerivative_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) {K : Set P} (hK : IsCompact K) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : Point P), z.1 ∈ K → ∀ (k : TorusInverse.Frequency), ‖multiplierTermDerivative m f k z‖ ≤ C * (TorusInverse.weight k ^ 4)⁻¹

theorem NavierStokes.SmoothFamilyTorusInverse.hasFDerivAt_applyMultiplier {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (z : Point P) : HasFDerivAt (applyMultiplier m f) (∑' (k : TorusInverse.Frequency), multiplierTermDerivative m f k z) z

theorem NavierStokes.SmoothFamilyTorusInverse.fderiv_applyMultiplier {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (z : Point P) : fderiv ℝ (applyMultiplier m f) z = ∑ i : BasisIndex P, (parameterLift i) (applyMultiplier m (parameterPartial (parameterBasis i) f) z) + torusLiftX (applyMultiplier (ParametricTorusInverse.multiplierX m) f z) + torusLiftY (applyMultiplier (ParametricTorusInverse.multiplierY m) f z)

theorem NavierStokes.SmoothFamilyTorusInverse.applyMultiplier_smooth_nat {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (n : ℕ) {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑n) (applyMultiplier m f)

theorem NavierStokes.SmoothFamilyTorusInverse.applyMultiplier_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑⊤) (applyMultiplier m f)

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑⊤) (inverse d f)

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_periodic {P : Type} (d : TorusInverse.Direction) (f : Source P) : Periodic (inverse d f)

theorem NavierStokes.SmoothFamilyTorusInverse.mean_applyMultiplier {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (p : P) : mean (applyMultiplier m f) p = m 0 * mean f p

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_zeroMean {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ZeroMean (inverse d f)

noncomputable def NavierStokes.SmoothFamilyTorusInverse.directionalPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : TorusInverse.Direction) (f : Source P) (z : Point P) : ℂ

Directional partial, given by fderiv ℝ f z (0, vector d).

Equations

• NavierStokes.SmoothFamilyTorusInverse.directionalPartial d f z = (fderiv ℝ f z) (0, NavierStokes.TorusInverse.vector d)

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_solves {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (hm : ZeroMean f) : directionalPartial d (inverse d f) = f

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_preserves_parameter_support {P : Type} (d : TorusInverse.Direction) (f : Source P) (S : Set P) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (p : P) : p ∉ S → ∀ (Y : TorusInverse.Plane), inverse d f (p, Y) = 0

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_applyMultiplier {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {m : TorusInverse.Frequency → ℂ} (hm : ParametricTorusInverse.PolynomialGrowth m) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (v : P) : parameterPartial v (applyMultiplier m f) = applyMultiplier m (parameterPartial v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterPartial_inverse {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (v : P) : parameterPartial v (inverse d f) = inverse d (parameterPartial v f)

def NavierStokes.SmoothFamilyTorusInverse.JetBound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : Source P) (S : Set P) (n : ℕ) (C : ℝ) : Prop

A prefix of actual full joint Fréchet-jet bounds on a parameter set. The torus argument ranges over the whole universal cover.

Equations

• NavierStokes.SmoothFamilyTorusInverse.JetBound f S n C = ∀ j ≤ n, ∀ p ∈ S, ∀ (Y : NavierStokes.TorusInverse.Plane), ‖iteratedFDeriv ℝ j f (p, Y)‖ ≤ C

theorem NavierStokes.SmoothFamilyTorusInverse.JetBound.mono_order {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} {S : Set P} {n m : ℕ} {C : ℝ} (h : JetBound f S n C) (hm : m ≤ n) : JetBound f S m C

theorem NavierStokes.SmoothFamilyTorusInverse.JetBound.fixedPartial {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) {S : Set P} {n : ℕ} {C : ℝ} (h : JetBound f S (n + 1) C) (v : Point P) : JetBound (SmoothFamilyTorusInverse.fixedPartial v f) S n (‖v‖ * C)

theorem NavierStokes.SmoothFamilyTorusInverse.norm_torusXJet_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (z : Point P) : ‖torusXJet n f z‖ ≤ ‖iteratedFDeriv ℝ n f z‖

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_swapTorus {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : Source P) (n : ℕ) (z : Point P) : ‖iteratedFDeriv ℝ n (swapTorus f) z‖ = ‖iteratedFDeriv ℝ n f (z.1, z.2.2, z.2.1)‖

theorem NavierStokes.SmoothFamilyTorusInverse.coefficient_moment_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) {S : Set P} (l : ℕ) {C : ℝ} (h : JetBound f S (l + 4) C) (p : P) (hps : p ∈ S) : TorusInverse.coeffSeminorm l (coefficient f p) ≤ 3 ^ (l + 4) * C * ∑' (k : TorusInverse.Frequency), (TorusInverse.weight k ^ 4)⁻¹

noncomputable def NavierStokes.SmoothFamilyTorusInverse.multiplierJetConstant {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] : ℕ → ℕ → ℝ

Multiplier jet constant used in smooth family torus inverse.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.SmoothFamilyTorusInverse.multiplierJetConstant 0 x✝ = 3 ^ (x✝ + 4) * ∑' (k : NavierStokes.TorusInverse.Frequency), (NavierStokes.TorusInverse.weight k ^ 4)⁻¹

theorem NavierStokes.SmoothFamilyTorusInverse.multiplierJetConstant_nonneg {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (n l : ℕ) : 0 ≤ multiplierJetConstant n l

theorem NavierStokes.SmoothFamilyTorusInverse.norm_jet_applyMultiplier_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (n l : ℕ) {m : TorusInverse.Frequency → ℂ} {B : ℝ} (hB : 0 ≤ B) (hm : ∀ (k : TorusInverse.Frequency), ‖m k‖ ≤ B * TorusInverse.weight k ^ l) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) {S : Set P} {C : ℝ} (hC : 0 ≤ C) (h : JetBound f S (n + l + 4) C) (p : P) (hps : p ∈ S) (Y : TorusInverse.Plane) : ‖iteratedFDeriv ℝ n (applyMultiplier m f) (p, Y)‖ ≤ multiplierJetConstant n l * B * C

The loss l+4 comes only from the order-l multiplier and the summable two-dimensional lattice majorant; it does not grow with jet order.

theorem NavierStokes.SmoothFamilyTorusInverse.applyMultiplier_finiteJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (n l : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (m : TorusInverse.Frequency → ℂ) (B : ℝ), 0 ≤ B → (∀ (k : TorusInverse.Frequency), ‖m k‖ ≤ B * TorusInverse.weight k ^ l) → ∀ (f : Source P) (S : Set P) (C : ℝ), ContDiff ℝ (↑⊤) f → Periodic f → 0 ≤ C → JetBound f S (n + l + 4) C → JetBound (applyMultiplier m f) S n (K * B * C)

theorem NavierStokes.SmoothFamilyTorusInverse.inverse_finiteJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) (n : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Source P) (S : Set P) (C : ℝ), ContDiff ℝ (↑⊤) f → Periodic f → 0 ≤ C → JetBound f S (n + 5) C → JetBound (inverse d f) S n (K * C)

Uniform full-tensor bound with five torus derivatives lost. The constant is chosen before the source, parameter set, or input bound.

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterJet {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (q : ℕ) (f : Source P) (z : Point P) : P [×q]→L[ℝ] ℂ

Parameter jet, given by (iteratedFDeriv ℝ q f z).compContinuousLinearMap (fun _ => ContinuousLinearMap.inl ℝ P Plane).

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterJet q f z = (iteratedFDeriv ℝ q f z).compContinuousLinearMap fun (x : Fin q) => ContinuousLinearMap.inl ℝ P NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.SmoothFamilyTorusInverse.parameterJetApply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (q : ℕ) (v : Fin q → P) (f : Source P) : Source P

Parameter jet apply, defined pointwise by parameterJet q f z v.

Equations

• NavierStokes.SmoothFamilyTorusInverse.parameterJetApply q v f z = (NavierStokes.SmoothFamilyTorusInverse.parameterJet q f z) v

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJet_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (q : ℕ) : ContDiff ℝ (↑⊤) (parameterJet q f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJetApply_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (q : ℕ) (v : Fin q → P) : ContDiff ℝ (↑⊤) (parameterJetApply q v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJet_eq_slice {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (q : ℕ) (p : P) (Y : TorusInverse.Plane) : parameterJet q f (p, Y) = iteratedFDeriv ℝ q (fun (t : P) => f (t, Y)) p

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJetApply_succ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (q : ℕ) (v : Fin (q + 1) → P) : parameterJetApply (q + 1) v f = parameterPartial (v 0) (parameterJetApply q (Fin.tail v) f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJetApply_periodic {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (q : ℕ) (v : Fin q → P) : Periodic (parameterJetApply q v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJetApply_inverse {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (q : ℕ) (v : Fin q → P) : parameterJetApply q v (inverse d f) = inverse d (parameterJetApply q v f)

theorem NavierStokes.SmoothFamilyTorusInverse.parameterJet_inverse {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (q : ℕ) (z : Point P) (v : Fin q → P) : (parameterJet q (inverse d f) z) v = inverse d (fun (w : Point P) => (parameterJet q f w) v) z

noncomputable def NavierStokes.SmoothFamilyTorusInverse.nonzeroMultiplier (k : TorusInverse.Frequency) : ℂ

Nonzero multiplier, with branches according to k = 0.

Equations

• NavierStokes.SmoothFamilyTorusInverse.nonzeroMultiplier k = if k = 0 then 0 else 1

theorem NavierStokes.SmoothFamilyTorusInverse.nonzeroMultiplier_growth : ParametricTorusInverse.PolynomialGrowth nonzeroMultiplier

noncomputable def NavierStokes.SmoothFamilyTorusInverse.nonbarPart {P : Type} (f : Source P) (z : Point P) : ℂ

Nonbar part, given by f z - mean f z.1.

Equations

• NavierStokes.SmoothFamilyTorusInverse.nonbarPart f z = f z - NavierStokes.SmoothFamilyTorusInverse.mean f z.1

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_eq_applyMultiplier {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : nonbarPart f = applyMultiplier nonzeroMultiplier f

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑⊤) (nonbarPart f)

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_periodic {P : Type} {f : Source P} (hp : Periodic f) : Periodic (nonbarPart f)

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_zeroMean {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ZeroMean (nonbarPart f)

theorem NavierStokes.SmoothFamilyTorusInverse.centered_inverse_solves {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : directionalPartial d (inverse d (nonbarPart f)) = nonbarPart f

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_finiteJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (n : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : Source P) (S : Set P) (C : ℝ), ContDiff ℝ (↑⊤) f → Periodic f → 0 ≤ C → JetBound f S (n + 4) C → JetBound (nonbarPart f) S n (K * C)

theorem NavierStokes.SmoothFamilyTorusInverse.nonbarPart_preserves_parameter_support {P : Type} (f : Source P) (S : Set P) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (p : P) : p ∉ S → ∀ (Y : TorusInverse.Plane), nonbarPart f (p, Y) = 0

noncomputable def NavierStokes.SmoothFamilyTorusInverse.mixedJet {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (q : ℕ) (w : List Bool) (f : Source P) (z : Point P) : P [×q]→L[ℝ] ℂ

Mixed jet, given by tensorTorusWord w (fun Y => parameterJet q f (z.1, Y)) z.2.

Equations

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

theorem NavierStokes.SmoothFamilyTorusInverse.mixedJet_apply {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (q : ℕ) (w : List Bool) (z : Point P) (v : Fin q → P) : (mixedJet q w f z) v = TorusInverse.derivativeWord w (slice (parameterJetApply q v f) z.1) z.2

theorem NavierStokes.SmoothFamilyTorusInverse.norm_derivativeWord_inverse_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (w : List Bool) (p : P) (Y : TorusInverse.Plane) {C : ℝ} (hzero : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖f (p, x, y)‖ ≤ C) (hfirst : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖SmoothFourierData.xJet (w.length + 5) (slice f p) (x, y)‖ ≤ C) (hsecond : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖SmoothFourierData.xJet (w.length + 5) (SmoothFourierData.swapFunction (slice f p)) (x, y)‖ ≤ C) : ‖TorusInverse.derivativeWord w (slice (inverse d f) p) Y‖ ≤ ParametricTorusInverse.mixedLossConstant w.length * C

theorem NavierStokes.SmoothFamilyTorusInverse.mixedJet_inverse_bound {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : Source P} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (q : ℕ) (w : List Bool) (S : Set P) {C : ℝ} (hC : 0 ≤ C) (hzero : ∀ p ∈ S, ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖parameterJet q f (p, x, y)‖ ≤ C) (hfirst : ∀ p ∈ S, ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖tensorTorusWord (List.replicate (w.length + 5) false) (fun (Y : TorusInverse.Plane) => parameterJet q f (p, Y)) (x, y)‖ ≤ C) (hsecond : ∀ p ∈ S, ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖tensorTorusWord (List.replicate (w.length + 5) false) (fun (Y : TorusInverse.Plane) => parameterJet q f (p, Y.2, Y.1)) (x, y)‖ ≤ C) (p : P) (hps : p ∈ S) (Y : TorusInverse.Plane) : ‖mixedJet q w (inverse d f) (p, Y)‖ ≤ ParametricTorusInverse.mixedLossConstant w.length * C

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_map {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) {f : D → E} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (z : D) : ‖iteratedFDeriv ℝ m (fun (x : D) => L (f x)) z‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ m f z‖

theorem NavierStokes.UniformFourierAlias.finiteJetBound_fixedPartial {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : D → E} (hf : ContDiff ℝ (↑⊤) f) {s : Set D} {C : ℝ} {m : ℕ} (hb : JetBounds.FiniteJetBound (m + 1) f s C) (v : D) (hv : ‖v‖ ≤ 1) : JetBounds.FiniteJetBound m (fun (x : D) => (fderiv ℝ f x) v) s C

theorem NavierStokes.UniformFourierAlias.sourceJet_mem {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (G : (ℝ × E → F) → Prop) (J : (ℝ × E → F) → ℝ × E → F) (hclosed : ∀ (f : ℝ × E → F), G f → G (RadialAlias.slowDeriv (J f))) (p : ℕ) {f : ℝ × E → F} (hf : G f) : G (RadialAlias.sourceJet J f p)

theorem NavierStokes.UniformFourierAlias.sourceJet_uniform_finiteJets {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (G : (ℝ × E → F) → Prop) (J : (ℝ × E → F) → ℝ × E → F) (s : Set (ℝ × E)) (loss : ℕ) (hclosed : ∀ (f : ℝ × E → F), G f → G (RadialAlias.slowDeriv (J f))) (hsmooth : ∀ (f : ℝ × E → F), G f → ContDiff ℝ (↑⊤) (J f)) (htame : ∀ (m : ℕ), ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + loss) f s C → JetBounds.FiniteJetBound m (J f) s (K * C)) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + (loss + 1) * p) f s C → JetBounds.FiniteJetBound m (RadialAlias.sourceJet J f p) s (K * C)

A finite-loss estimate for an actual operator propagates through the successive slow derivatives used in radial integration by parts. This lemma is instantiated below with the constructed torus inverse.

noncomputable def NavierStokes.UniformFourierAlias.exactAlias {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (χ : ℝ → ℝ) (M : ℝ) (v : E) (f : ℝ × E → F) (z : ℝ × E) : F

The exact defect in the compact transport primitive, with all auxiliary slow variables retained in E.

Equations

• NavierStokes.UniformFourierAlias.exactAlias χ M v f z = deriv χ z.1 • NavierStokes.TransportPrimitive.totalIntegral M v f z

theorem NavierStokes.UniformFourierAlias.exactAlias_smooth {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {χ : ℝ → ℝ} {f : ℝ × E → F} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (exactAlias χ M v f)

theorem NavierStokes.UniformFourierAlias.exactAlias_supported {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : E} {χ : ℝ → ℝ} {f : ℝ × E → F} (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) : RadialAlias.RadiallySupported a b (exactAlias χ M v f)

theorem NavierStokes.UniformFourierAlias.transport_compact_exactAlias {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M : ℝ} {v : E} {χ : ℝ → ℝ} {f : ℝ × E → F} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (z : ℝ × E) : TransportPrimitive.fixedDeriv (1, M • v) (TransportPrimitive.compactIntegral χ M v f) z = f z - exactAlias χ M v f z

theorem NavierStokes.UniformFourierAlias.totalIntegral_sourceJet_bound {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b M C : ℝ} {v : E} (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p m : ℕ) (hab : a ≤ b) (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) (hbound : JetBounds.FiniteJetBound m (RadialAlias.sourceJet J f p) (Prod.fst ⁻¹' Set.Icc a b) C) (j : ℕ) (hj : j ≤ m) (z : ℝ × E) : ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M v f) z‖ ≤ C * (b - a) * |M|⁻¹ ^ p

Repeated integration by parts for full derivative tensors. The last premise bounds genuine source jets, not the alias.

theorem NavierStokes.UniformFourierAlias.exactAlias_sourceJet_bound {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (M : ℝ) (v : E) (J : (ℝ × E → F) → ℝ × E → F) (f : ℝ × E → F) (p : ℕ) (C : ℝ), M ≠ 0 → 0 ≤ C → ContDiff ℝ (↑⊤) f → RadialAlias.RadiallySupported a b f → (∀ n < p, ContDiff ℝ (↑⊤) (J (RadialAlias.sourceJet J f n))) → (∀ n < p, RadialAlias.RadiallySupported a b (J (RadialAlias.sourceJet J f n))) → (∀ n < p, RadialAlias.directionalDeriv v (J (RadialAlias.sourceJet J f n)) = RadialAlias.sourceJet J f n) → JetBounds.FiniteJetBound m (RadialAlias.sourceJet J f p) (Prod.fst ⁻¹' Set.Icc a b) C → ∀ j ≤ m, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (exactAlias χ M v f) z‖ ≤ K * C * |M|⁻¹ ^ p

A source-independent constant for the compactification defect, retaining the entire cutoff Leibniz expansion.

theorem NavierStokes.UniformFourierAlias.totalIntegral_uniform_of_inverse {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {v : E} (G : (ℝ × E → F) → Prop) (J : (ℝ × E → F) → ℝ × E → F) (loss : ℕ) (hab : a ≤ b) (hregular : ∀ (f : ℝ × E → F), G f → ContDiff ℝ (↑⊤) f ∧ RadialAlias.RadiallySupported a b f) (hsmooth : ∀ (f : ℝ × E → F), G f → ContDiff ℝ (↑⊤) (J f)) (hsupport : ∀ (f : ℝ × E → F), G f → RadialAlias.RadiallySupported a b (J f)) (hsolve : ∀ (f : ℝ × E → F), G f → RadialAlias.directionalDeriv v (J f) = f) (hclosed : ∀ (f : ℝ × E → F), G f → G (RadialAlias.slowDeriv (J f))) (htame : ∀ (m : ℕ), ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + loss) f (Prod.fst ⁻¹' Set.Icc a b) C → JetBounds.FiniteJetBound m (J f) (Prod.fst ⁻¹' Set.Icc a b) (K * C)) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + (loss + 1) * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M v f) z‖ ≤ K * C * |M|⁻¹ ^ p

theorem NavierStokes.UniformFourierAlias.exactAlias_uniform_of_inverse {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {a b : ℝ} {v : E} {χ : ℝ → ℝ} (G : (ℝ × E → F) → Prop) (J : (ℝ × E → F) → ℝ × E → F) (loss : ℕ) (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (hregular : ∀ (f : ℝ × E → F), G f → ContDiff ℝ (↑⊤) f ∧ RadialAlias.RadiallySupported a b f) (hsmooth : ∀ (f : ℝ × E → F), G f → ContDiff ℝ (↑⊤) (J f)) (hsupport : ∀ (f : ℝ × E → F), G f → RadialAlias.RadiallySupported a b (J f)) (hsolve : ∀ (f : ℝ × E → F), G f → RadialAlias.directionalDeriv v (J f) = f) (hclosed : ∀ (f : ℝ × E → F), G f → G (RadialAlias.slowDeriv (J f))) (htame : ∀ (m : ℕ), ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + loss) f (Prod.fst ⁻¹' Set.Icc a b) C → JetBounds.FiniteJetBound m (J f) (Prod.fst ⁻¹' Set.Icc a b) (K * C)) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × E → F), G f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + (loss + 1) * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ j (exactAlias χ M v f) z‖ ≤ K * C * |M|⁻¹ ^ p

noncomputable def NavierStokes.UniformFourierAlias.complexify {D : Type} (f : D → ℝ) (z : D) : ℂ

Complexify, given by f z.

Equations

• NavierStokes.UniformFourierAlias.complexify f z = ↑(f z)

theorem NavierStokes.UniformFourierAlias.complexify_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (complexify f)

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_complexify {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {f : D → ℝ} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (z : D) : ‖iteratedFDeriv ℝ m (complexify f) z‖ = ‖iteratedFDeriv ℝ m f z‖

theorem NavierStokes.UniformFourierAlias.complexify_supported {E : Type} {a b : ℝ} {f : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (complexify f)

theorem NavierStokes.UniformFourierAlias.totalIntegral_complexify {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℝ) (v : E) (f : ℝ × E → ℝ) : TransportPrimitive.totalIntegral M v (complexify f) = complexify (TransportPrimitive.totalIntegral M v f)

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_totalIntegral_complexify {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b M : ℝ} {v : E} {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (m : ℕ) (z : ℝ × E) : ‖iteratedFDeriv ℝ m (TransportPrimitive.totalIntegral M v (complexify f)) z‖ = ‖iteratedFDeriv ℝ m (TransportPrimitive.totalIntegral M v f) z‖

theorem NavierStokes.UniformFourierAlias.exactAlias_complexify {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (χ : ℝ → ℝ) (M : ℝ) (v : E) (f : ℝ × E → ℝ) : exactAlias χ M v (complexify f) = complexify (exactAlias χ M v f)

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_exactAlias_complexify {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b M : ℝ} {v : E} {χ : ℝ → ℝ} {f : ℝ × E → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (m : ℕ) (z : ℝ × E) : ‖iteratedFDeriv ℝ m (exactAlias χ M v (complexify f)) z‖ = ‖iteratedFDeriv ℝ m (exactAlias χ M v f) z‖

noncomputable def NavierStokes.UniformFourierAlias.toProduct {S F : Type} (f : ℝ × S × TorusInverse.Plane → F) (z : (ℝ × S) × TorusInverse.Plane) : F

Reassociate radial, slow, and torus variables without changing the norm.

Equations

• NavierStokes.UniformFourierAlias.toProduct f z = f (z.1.1, z.1.2, z.2)

noncomputable def NavierStokes.UniformFourierAlias.fromProduct {S F : Type} (f : (ℝ × S) × TorusInverse.Plane → F) (z : ℝ × S × TorusInverse.Plane) : F

From product, given by f ((z.1, z.2.1), z.2.2).

Equations

• NavierStokes.UniformFourierAlias.fromProduct f z = f ((z.1, z.2.1), z.2.2)

@[simp]

theorem NavierStokes.UniformFourierAlias.fromProduct_toProduct {S F : Type} (f : ℝ × S × TorusInverse.Plane → F) : fromProduct (toProduct f) = f

@[simp]

theorem NavierStokes.UniformFourierAlias.toProduct_fromProduct {S F : Type} (f : (ℝ × S) × TorusInverse.Plane → F) : toProduct (fromProduct f) = f

theorem NavierStokes.UniformFourierAlias.toProduct_smooth {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × S × TorusInverse.Plane → F} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (toProduct f)

theorem NavierStokes.UniformFourierAlias.fromProduct_smooth {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : (ℝ × S) × TorusInverse.Plane → F} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (fromProduct f)

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_toProduct {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ × S × TorusInverse.Plane → F) (m : ℕ) (z : (ℝ × S) × TorusInverse.Plane) : ‖iteratedFDeriv ℝ m (toProduct f) z‖ = ‖iteratedFDeriv ℝ m f (z.1.1, z.1.2, z.2)‖

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_fromProduct {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : (ℝ × S) × TorusInverse.Plane → F) (m : ℕ) (z : ℝ × S × TorusInverse.Plane) : ‖iteratedFDeriv ℝ m (fromProduct f) z‖ = ‖iteratedFDeriv ℝ m f ((z.1, z.2.1), z.2.2)‖

noncomputable def NavierStokes.UniformFourierAlias.sourceMean {S F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ × S × TorusInverse.Plane → F) (p : ℝ × S) : F

Source mean, given by FourierAlias.torusMean (fun Y => f (p.1, (p.2, Y))).

Equations

• NavierStokes.UniformFourierAlias.sourceMean f p = NavierStokes.FourierAlias.torusMean fun (Y : NavierStokes.TorusInverse.Plane) => f (p.1, p.2, Y)

noncomputable def NavierStokes.UniformFourierAlias.SourcePeriodic {S F : Type} (f : ℝ × S × TorusInverse.Plane → F) : Prop

Source periodic, given by ∀ U s, FourierAlias.TorusPeriodic (fun Y => f (U, (s, Y))).

Equations

• NavierStokes.UniformFourierAlias.SourcePeriodic f = ∀ (U : ℝ) (s : S), NavierStokes.FourierAlias.TorusPeriodic fun (Y : NavierStokes.TorusInverse.Plane) => f (U, s, Y)

noncomputable def NavierStokes.UniformFourierAlias.radialSlice {S F : Type} (f : ℝ × S × TorusInverse.Plane → F) (s : S) (z : ℝ × TorusInverse.Plane) : F

Radial slice, given by f (z.1, (s, z.2)).

Equations

• NavierStokes.UniformFourierAlias.radialSlice f s z = f (z.1, s, z.2)

theorem NavierStokes.UniformFourierAlias.radialSlice_smooth {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × S × TorusInverse.Plane → F} (hf : ContDiff ℝ (↑⊤) f) (s : S) : ContDiff ℝ (↑⊤) (radialSlice f s)

theorem NavierStokes.UniformFourierAlias.radialSlice_supported {S F : Type} [NormedAddCommGroup F] {a b : ℝ} {f : ℝ × S × TorusInverse.Plane → F} (hs : RadialAlias.RadiallySupported a b f) (s : S) : RadialAlias.RadiallySupported a b (radialSlice f s)

theorem NavierStokes.UniformFourierAlias.totalIntegral_radialSlice {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] (M : ℝ) (v : TorusInverse.Plane) (f : ℝ × S × TorusInverse.Plane → F) (U : ℝ) (s : S) (Y : TorusInverse.Plane) : TransportPrimitive.totalIntegral M (0, v) f (U, s, Y) = TransportPrimitive.totalIntegral M v (radialSlice f s) (U, Y)

theorem NavierStokes.UniformFourierAlias.sourceMean_totalIntegral {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : TorusInverse.Plane} {f : ℝ × S × TorusInverse.Plane → F} (hab : a ≤ b) (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (hs : RadialAlias.RadiallySupported a b f) (U : ℝ) (s : S) : sourceMean (TransportPrimitive.totalIntegral M (0, v) f) (U, s) = ∫ (u : ℝ) in a..b, sourceMean f (u, s)

theorem NavierStokes.UniformFourierAlias.exactAlias_sourceMean_zero {S F : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b M : ℝ} {v : TorusInverse.Plane} {f : ℝ × S × TorusInverse.Plane → F} (χ : ℝ → ℝ) (hab : a ≤ b) (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (s : S), ∫ (u : ℝ) in a..b, sourceMean f (u, s) = 0) (p : ℝ × S) : sourceMean (exactAlias χ M (0, v) f) p = 0

theorem NavierStokes.UniformFourierAlias.sourceMean_complexify {S : Type} (f : ℝ × S × TorusInverse.Plane → ℝ) (p : ℝ × S) : sourceMean (complexify f) p = ↑(sourceMean f p)

noncomputable def NavierStokes.UniformFourierAlias.ParameterPeriodic {P F : Type} (f : P × TorusInverse.Plane → F) : Prop

Parameter periodic, given by ∀ p, FourierAlias.TorusPeriodic (fun Y => f (p, Y)).

Equations

• NavierStokes.UniformFourierAlias.ParameterPeriodic f = ∀ (p : P), NavierStokes.FourierAlias.TorusPeriodic fun (Y : NavierStokes.TorusInverse.Plane) => f (p, Y)

noncomputable def NavierStokes.UniformFourierAlias.parameterMean {P F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : P × TorusInverse.Plane → F) (p : P) : F

Parameter mean, given by FourierAlias.torusMean (fun Y => f (p, Y)).

Equations

• NavierStokes.UniformFourierAlias.parameterMean f p = NavierStokes.FourierAlias.torusMean fun (Y : NavierStokes.TorusInverse.Plane) => f (p, Y)

theorem NavierStokes.UniformFourierAlias.complexify_parameterPeriodic {P : Type} {f : P × TorusInverse.Plane → ℝ} (hp : ParameterPeriodic f) : SmoothFamilyTorusInverse.Periodic (complexify f)

theorem NavierStokes.UniformFourierAlias.parameterMean_complexify {P : Type} (f : P × TorusInverse.Plane → ℝ) (p : P) : parameterMean (complexify f) p = ↑(parameterMean f p)

theorem NavierStokes.UniformFourierAlias.familyMean_eq_parameterMean {P : Type} (f : P × TorusInverse.Plane → ℂ) (p : P) : SmoothFamilyTorusInverse.mean f p = parameterMean f p

theorem NavierStokes.UniformFourierAlias.torusMean_map {F H : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace F] [CompleteSpace H] (L : F →L[ℝ] H) {f : TorusInverse.Plane → F} (hf : Continuous f) : (FourierAlias.torusMean fun (Y : TorusInverse.Plane) => L (f Y)) = L (FourierAlias.torusMean f)

noncomputable def NavierStokes.UniformFourierAlias.realInverse {P : Type} (d : TorusInverse.Direction) (f : P × TorusInverse.Plane → ℝ) (z : P × TorusInverse.Plane) : ℝ

A genuine real directional inverse, obtained from the actual complex Fourier inverse by real part.

Equations

• NavierStokes.UniformFourierAlias.realInverse d f z = (NavierStokes.SmoothFamilyTorusInverse.inverse d (NavierStokes.UniformFourierAlias.complexify f) z).re

noncomputable def NavierStokes.UniformFourierAlias.realCentered {P : Type} (f : P × TorusInverse.Plane → ℝ) (z : P × TorusInverse.Plane) : ℝ

Real centered, given by f z - parameterMean f z.1.

Equations

• NavierStokes.UniformFourierAlias.realCentered f z = f z - NavierStokes.UniformFourierAlias.parameterMean f z.1

theorem NavierStokes.UniformFourierAlias.complexify_realCentered {P : Type} (f : P × TorusInverse.Plane → ℝ) : complexify (realCentered f) = SmoothFamilyTorusInverse.nonbarPart (complexify f)

theorem NavierStokes.UniformFourierAlias.realCentered_eq_re_nonbar {P : Type} (f : P × TorusInverse.Plane → ℝ) : realCentered f = fun (z : SmoothFamilyTorusInverse.Point P) => (SmoothFamilyTorusInverse.nonbarPart (complexify f) z).re

theorem NavierStokes.UniformFourierAlias.realCentered_periodic {P : Type} {f : P × TorusInverse.Plane → ℝ} (hp : ParameterPeriodic f) : ParameterPeriodic (realCentered f)

theorem NavierStokes.UniformFourierAlias.realCentered_preserves_parameter_support {P : Type} (f : P × TorusInverse.Plane → ℝ) (S : Set P) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (p : P) : p ∉ S → ∀ (Y : TorusInverse.Plane), realCentered f (p, Y) = 0

theorem NavierStokes.UniformFourierAlias.realInverse_periodic {P : Type} (d : TorusInverse.Direction) (f : P × TorusInverse.Plane → ℝ) : ParameterPeriodic (realInverse d f)

theorem NavierStokes.UniformFourierAlias.realInverse_preserves_parameter_support {P : Type} (d : TorusInverse.Direction) (f : P × TorusInverse.Plane → ℝ) (S : Set P) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (p : P) : p ∉ S → ∀ (Y : TorusInverse.Plane), realInverse d f (p, Y) = 0

theorem NavierStokes.UniformFourierAlias.realCentered_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) : ContDiff ℝ (↑⊤) (realCentered f)

theorem NavierStokes.UniformFourierAlias.realCentered_zeroMean {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) (p : P) : parameterMean (realCentered f) p = 0

theorem NavierStokes.UniformFourierAlias.realInverse_smooth {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) : ContDiff ℝ (↑⊤) (realInverse d f)

theorem NavierStokes.UniformFourierAlias.realInverse_zeroMean {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) (p : P) : parameterMean (realInverse d f) p = 0

theorem NavierStokes.UniformFourierAlias.realInverse_solves {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) (hm : ∀ (p : P), parameterMean f p = 0) (z : P × TorusInverse.Plane) : (fderiv ℝ (realInverse d f) z) (0, TorusInverse.vector d) = f z

theorem NavierStokes.UniformFourierAlias.norm_iteratedFDeriv_realInverse_le {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) {f : P × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : ParameterPeriodic f) (m : ℕ) (z : P × TorusInverse.Plane) : ‖iteratedFDeriv ℝ m (realInverse d f) z‖ ≤ ‖iteratedFDeriv ℝ m (SmoothFamilyTorusInverse.inverse d (complexify f)) z‖

theorem NavierStokes.UniformFourierAlias.realInverse_finiteJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (d : TorusInverse.Direction) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : P × TorusInverse.Plane → ℝ) (A : Set P) (C : ℝ), ContDiff ℝ (↑⊤) f → ParameterPeriodic f → 0 ≤ C → (∀ j ≤ m + 5, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j f (p, Y)‖ ≤ C) → ∀ j ≤ m, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j (realInverse d f) (p, Y)‖ ≤ K * C

theorem NavierStokes.UniformFourierAlias.realCentered_finiteJets {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : P × TorusInverse.Plane → ℝ) (A : Set P) (C : ℝ), ContDiff ℝ (↑⊤) f → ParameterPeriodic f → 0 ≤ C → (∀ j ≤ m + 4, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j f (p, Y)‖ ≤ C) → ∀ j ≤ m, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j (realCentered f) (p, Y)‖ ≤ K * C

noncomputable def NavierStokes.UniformFourierAlias.familyInverse {S : Type} (d : TorusInverse.Direction) (f : ℝ × S × TorusInverse.Plane → ℂ) : ℝ × S × TorusInverse.Plane → ℂ

Family inverse, given by fromProduct (SmoothFamilyTorusInverse.inverse d (toProduct f)).

Equations

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

theorem NavierStokes.UniformFourierAlias.mean_toProduct {S : Type} (f : ℝ × S × TorusInverse.Plane → ℂ) (p : ℝ × S) : SmoothFamilyTorusInverse.mean (toProduct f) p = sourceMean f p

noncomputable def NavierStokes.UniformFourierAlias.realCenterSource {S : Type} (f : ℝ × S × TorusInverse.Plane → ℝ) : ℝ × S × TorusInverse.Plane → ℝ

Real center source, given by fromProduct (realCentered (toProduct f)).

Equations

• NavierStokes.UniformFourierAlias.realCenterSource f = NavierStokes.UniformFourierAlias.fromProduct (NavierStokes.UniformFourierAlias.realCentered (NavierStokes.UniformFourierAlias.toProduct f))

theorem NavierStokes.UniformFourierAlias.realCenterSource_apply {S : Type} (f : ℝ × S × TorusInverse.Plane → ℝ) (z : ℝ × S × TorusInverse.Plane) : realCenterSource f z = f z - sourceMean f (z.1, z.2.1)

theorem NavierStokes.UniformFourierAlias.realCenterSource_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {f : ℝ × S × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) : ContDiff ℝ (↑⊤) (realCenterSource f)

theorem NavierStokes.UniformFourierAlias.realCenterSource_periodic {S : Type} {f : ℝ × S × TorusInverse.Plane → ℝ} (hp : SourcePeriodic f) : SourcePeriodic (realCenterSource f)

theorem NavierStokes.UniformFourierAlias.realCenterSource_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : ℝ × S × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (p : ℝ × S) : sourceMean (realCenterSource f) p = 0

theorem NavierStokes.UniformFourierAlias.realCenterSource_supported {S : Type} {a b : ℝ} {f : ℝ × S × TorusInverse.Plane → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (realCenterSource f)

theorem NavierStokes.UniformFourierAlias.totalIntegral_realCenterSource {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b M : ℝ} {v : TorusInverse.Plane} {f : ℝ × S × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (s : S), ∫ (U : ℝ) in a..b, sourceMean f (U, s) = 0) (z : ℝ × S × TorusInverse.Plane) : TransportPrimitive.totalIntegral M (0, v) (realCenterSource f) z = TransportPrimitive.totalIntegral M (0, v) f z

theorem NavierStokes.UniformFourierAlias.exactAlias_eq_realCenterSource {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b M : ℝ} {v : TorusInverse.Plane} {f : ℝ × S × TorusInverse.Plane → ℝ} (χ : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (s : S), ∫ (U : ℝ) in a..b, sourceMean f (U, s) = 0) : exactAlias χ M (0, v) f = exactAlias χ M (0, v) (realCenterSource f)

theorem NavierStokes.UniformFourierAlias.periodic_toProduct {S : Type} {f : ℝ × S × TorusInverse.Plane → ℂ} (hp : SourcePeriodic f) : SmoothFamilyTorusInverse.Periodic (toProduct f)

theorem NavierStokes.UniformFourierAlias.familyInverse_smooth {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {f : ℝ × S × TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFamilyTorusInverse.Periodic (toProduct f)) : ContDiff ℝ (↑⊤) (familyInverse d f)

theorem NavierStokes.UniformFourierAlias.familyInverse_periodic {S : Type} (d : TorusInverse.Direction) (f : ℝ × S × TorusInverse.Plane → ℂ) : SmoothFamilyTorusInverse.Periodic (toProduct (familyInverse d f))

theorem NavierStokes.UniformFourierAlias.familyInverse_zeroMean {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d : TorusInverse.Direction) {f : ℝ × S × TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFamilyTorusInverse.Periodic (toProduct f)) : SmoothFamilyTorusInverse.ZeroMean (toProduct (familyInverse d f))

theorem NavierStokes.UniformFourierAlias.familyInverse_supported {S : Type} (d : TorusInverse.Direction) {a b : ℝ} {f : ℝ × S × TorusInverse.Plane → ℂ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (familyInverse d f)

theorem NavierStokes.UniformFourierAlias.toProduct_slowDeriv {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : ℝ × S × TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) : toProduct (RadialAlias.slowDeriv f) = SmoothFamilyTorusInverse.parameterPartial (1, 0) (toProduct f)

theorem NavierStokes.UniformFourierAlias.familyInverse_solves {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {f : ℝ × S × TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : SmoothFamilyTorusInverse.Periodic (toProduct f)) (hm : SmoothFamilyTorusInverse.ZeroMean (toProduct f)) : RadialAlias.directionalDeriv (0, TorusInverse.vector d) (familyInverse d f) = f

noncomputable def NavierStokes.UniformFourierAlias.Admissible {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (a b : ℝ) (f : ℝ × S × TorusInverse.Plane → ℂ) : Prop

Admissible, constructed using ContDiff.

Equations

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

theorem NavierStokes.UniformFourierAlias.admissible_step {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} {f : ℝ × S × TorusInverse.Plane → ℂ} (hf : Admissible a b f) : Admissible a b (RadialAlias.slowDeriv (familyInverse d f))

theorem NavierStokes.UniformFourierAlias.familyInverse_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) (a b : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℂ) (C : ℝ), ContDiff ℝ (↑⊤) f → SmoothFamilyTorusInverse.Periodic (toProduct f) → 0 ≤ C → JetBounds.FiniteJetBound (m + 5) f (Prod.fst ⁻¹' Set.Icc a b) C → JetBounds.FiniteJetBound m (familyInverse d f) (Prod.fst ⁻¹' Set.Icc a b) (K * C)

theorem NavierStokes.UniformFourierAlias.realCenterSource_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (a b : ℝ) (m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℝ) (C : ℝ), ContDiff ℝ (↑⊤) f → SourcePeriodic f → 0 ≤ C → JetBounds.FiniteJetBound (m + 4) f (Prod.fst ⁻¹' Set.Icc a b) C → JetBounds.FiniteJetBound m (realCenterSource f) (Prod.fst ⁻¹' Set.Icc a b) (K * C)

theorem NavierStokes.UniformFourierAlias.totalIntegral_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} (hab : a ≤ b) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℂ), Admissible a b f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + 6 * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

Actual, source-uniform finite-seminorm estimate for the translated total integral. Every integration by parts consumes one radial derivative and five orders for the genuine torus inverse.

theorem NavierStokes.UniformFourierAlias.exactAlias_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℂ), Admissible a b f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + 6 * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

The retained alias has the same arbitrary inverse-frequency gain, with all source dependence confined to a finite actual derivative bound.

theorem NavierStokes.UniformFourierAlias.meanClass_global_finiteJets {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → ℝ × E → F} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (q : ℕ), ∀ (n : ℕ), JetBounds.FiniteJetBound m (f n) Set.univ (C * ε n ^ α * S n ^ q)

The flat radial weight absorbs every fixed inverse-edge power, giving a global finite seminorm bound for a genuine mean-class family.

theorem NavierStokes.UniformFourierAlias.meanClass_normalizeSource {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b d cL cR : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {α : ℝ} {f : ℕ → ℝ × E → F} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε S hε hεone hS) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData (a ^ d) (b ^ d) (d ^ 2 * cL) (d ^ 2 * cR) ⋯ ⋯ ⋯ ε S hε hεone hS) α fun (n : ℕ) => RadialPullback.normalizeSource d a (f n)

The actual power-chart normalization transports the source family class; all constants are uniform in the band and every auxiliary variable.

theorem NavierStokes.UniformFourierAlias.fiberOperator_preserves_meanClass {S F H : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ((ℝ × S) × TorusInverse.Plane → F) → (ℝ × S) × TorusInverse.Plane → H) (loss : ℕ) (hTsmooth : ∀ (f : (ℝ × S) × TorusInverse.Plane → F), ContDiff ℝ (↑⊤) f → ParameterPeriodic f → ContDiff ℝ (↑⊤) (T f)) (hTbound : ∀ (m : ℕ), ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : (ℝ × S) × TorusInverse.Plane → F) (A : Set (ℝ × S)) (C : ℝ), ContDiff ℝ (↑⊤) f → ParameterPeriodic f → 0 ≤ C → (∀ j ≤ m + loss, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j f (p, Y)‖ ≤ C) → ∀ j ≤ m, ∀ p ∈ A, ∀ (Y : TorusInverse.Plane), ‖iteratedFDeriv ℝ j (T f) (p, Y)‖ ≤ K * C) {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {α : ℝ} {f : ℕ → ℝ × S × TorusInverse.Plane → F} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => fromProduct (T (toProduct (f n)))

A proved finite loss on each parameter fiber preserves the actual all-order mean class, including its radial weight.

theorem NavierStokes.UniformFourierAlias.meanClass_realInverse {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {α : ℝ} {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => fromProduct (realInverse d (toProduct (f n)))

theorem NavierStokes.UniformFourierAlias.meanClass_realCenterSource {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR : ℝ} (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (ε R : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hR : ∀ (n : ℕ), 1 ≤ R n) {α : ℝ} {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData a b cL cR ha hcL hcR ε R hε hεone hR) α fun (n : ℕ) => realCenterSource (f n)

noncomputable def NavierStokes.UniformFourierAlias.bandSlow (n : ℕ) : ℝ

The actual slow scale, clipped only at the finitely many initial bands.

Equations

• NavierStokes.UniformFourierAlias.bandSlow n = max 1 (NavierStokes.ChartScales.S n)

theorem NavierStokes.UniformFourierAlias.one_le_bandSlow (n : ℕ) : 1 ≤ bandSlow n

theorem NavierStokes.UniformFourierAlias.bandSlow_eventually_eq : ∀ᶠ (n : ℕ) in Filter.atTop, bandSlow n = ChartScales.S n

theorem NavierStokes.UniformFourierAlias.frequency_gain_absorbs_family_growth {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 : ℕ), ∀ (q : ℕ) (C : ℝ), 0 ≤ C → ∀ᶠ (n : ℕ) in Filter.atTop, C * ChartScales.epsilon h n ^ α * bandSlow n ^ q * |M n|⁻¹ ^ p ≤ C * ChartScales.epsilon h n ^ N

Choose the number of integrations by parts before learning the finite polynomial slow-scale loss of the required source seminorm.

noncomputable def NavierStokes.UniformFourierAlias.chartStrip {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b cL cR : ℝ) (ha : 0 < a) (hcL : 0 < cL) (hcR : 0 < cR) (h : ℝ) (hh : 0 < h) : WeightedClasses.StripData (ℝ × E)

The concrete radial strip with the manuscript's actual band scales.

Equations

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

theorem NavierStokes.UniformFourierAlias.meanClass_alias_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b cL cR h α : ℝ} (ha : 0 < a) (hab : a ≤ b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {f : ℕ → ℝ × S × TorusInverse.Plane → ℂ} (hf : WeightedClasses.MeanClass (chartStrip a b cL cR ha hcL hcR h hh) α f) (hgood : ∀ (n : ℕ), Admissible a b (f n)) {M : ℕ → ℝ} {κ A growth : ℝ} (hκ : 0 < κ) (hM : ∀ᶠ (n : ℕ) in Filter.atTop, M n ≠ 0) (hfrequency : ∀ᶠ (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 : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ (M n) (0, TorusInverse.vector d) (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N

Band-dependent sources in the actual all-order mean class have uniformly superflat aliases. The proof chooses one finite IBP order before extracting the required source seminorm and its polynomial growth degree.

theorem NavierStokes.UniformFourierAlias.admissible_complexify {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {f : ℝ × S × TorusInverse.Plane → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : SourcePeriodic f) (hm : ∀ (p : ℝ × S), sourceMean f p = 0) (hs : RadialAlias.RadiallySupported a b f) : Admissible a b (complexify f)

theorem NavierStokes.UniformFourierAlias.real_totalIntegral_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} (hab : a ≤ b) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℝ), ContDiff ℝ (↑⊤) f → SourcePeriodic f → (∀ (q : ℝ × S), sourceMean f q = 0) → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + 6 * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (TransportPrimitive.totalIntegral M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

theorem NavierStokes.UniformFourierAlias.real_exactAlias_finiteJets {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℝ), ContDiff ℝ (↑⊤) f → SourcePeriodic f → (∀ (q : ℝ × S), sourceMean f q = 0) → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + 6 * p) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

theorem NavierStokes.UniformFourierAlias.real_exactAlias_finiteJets_of_integratedMean_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b : ℝ} {χ : ℝ → ℝ} (hab : a ≤ b) (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) (m p : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (f : ℝ × S × TorusInverse.Plane → ℝ), ContDiff ℝ (↑⊤) f → SourcePeriodic f → (∀ (s : S), ∫ (U : ℝ) in a..b, sourceMean f (U, s) = 0) → RadialAlias.RadiallySupported a b f → ∀ (C : ℝ), 0 ≤ C → JetBounds.FiniteJetBound (m + 6 * p + 4) f (Prod.fst ⁻¹' Set.Icc a b) C → ∀ (M : ℝ), M ≠ 0 → ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ M (0, TorusInverse.vector d) f) z‖ ≤ K * C * |M|⁻¹ ^ p

Only the integrated torus mean must vanish. Mean subtraction costs four extra finite derivative orders and changes the exact alias by zero.

theorem NavierStokes.UniformFourierAlias.realMeanClass_alias_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b cL cR h α : ℝ} (ha : 0 < a) (hab : a ≤ b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) (hm : ∀ (n : ℕ) (p : ℝ × S), sourceMean (f n) p = 0) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) {M : ℕ → ℝ} {κ A growth : ℝ} (hκ : 0 < κ) (hM : ∀ᶠ (n : ℕ) in Filter.atTop, M n ≠ 0) (hfrequency : ∀ᶠ (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 : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ (M n) (0, TorusInverse.vector d) (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N

theorem NavierStokes.UniformFourierAlias.radial_realMeanClass_alias_superflat {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR h α : ℝ} (ha : 0 < a) (hab : a ≤ b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) (hm : ∀ (n : ℕ) (p : ℝ × S), sourceMean (f n) p = 0) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ (ChartScales.radialCoefficient h n) (0, TorusInverse.vector TorusInverse.Direction.radial) (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N

theorem NavierStokes.UniformFourierAlias.realMeanClass_alias_superflat_of_integratedMean_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] (d : TorusInverse.Direction) {a b cL cR h α : ℝ} (ha : 0 < a) (hab : a ≤ b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) (hm : ∀ (n : ℕ) (s : S), ∫ (U : ℝ) in a..b, sourceMean (f n) (U, s) = 0) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) {M : ℕ → ℝ} {κ A growth : ℝ} (hκ : 0 < κ) (hM : ∀ᶠ (n : ℕ) in Filter.atTop, M n ≠ 0) (hfrequency : ∀ᶠ (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 : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ (M n) (0, TorusInverse.vector d) (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N

theorem NavierStokes.UniformFourierAlias.radial_realMeanClass_alias_superflat_of_integratedMean_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] [FiniteDimensional ℝ S] {a b cL cR h α : ℝ} (ha : 0 < a) (hab : a ≤ b) (hcL : 0 < cL) (hcR : 0 < cR) (hh : 0 < h) {χ : ℝ → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hleft : ∀ u ≤ a, χ u = 0) (hright : ∀ (u : ℝ), b ≤ u → χ u = 1) {f : ℕ → ℝ × S × TorusInverse.Plane → ℝ} (hf : WeightedClasses.MeanClass (chartStrip a b cL cR ha hcL hcR h hh) α f) (hfc : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hp : ∀ (n : ℕ), SourcePeriodic (f n)) (hm : ∀ (n : ℕ) (s : S), ∫ (U : ℝ) in a..b, sourceMean (f n) (U, s) = 0) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported a b (f n)) (m N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ m, ∀ (z : ℝ × S × TorusInverse.Plane), ‖iteratedFDeriv ℝ j (exactAlias χ (ChartScales.radialCoefficient h n) (0, TorusInverse.vector TorusInverse.Direction.radial) (f n)) z‖ ≤ C * ChartScales.epsilon h n ^ N