The actual smooth torus inverse with an external real parameter

The coefficients are the integrals of the given function. Local uniform decay is obtained from genuine derivatives on compact parameter intervals.

@[reducible, inline]

abbrev NavierStokes.ParametricTorusInverse.Point : Type

Point: an abbreviation for ℝ × Plane.

Equations

• NavierStokes.ParametricTorusInverse.Point = (ℝ × NavierStokes.TorusInverse.Plane)

@[reducible, inline]

abbrev NavierStokes.ParametricTorusInverse.Source : Type

Source: an abbreviation for Point → ℂ.

Equations

• NavierStokes.ParametricTorusInverse.Source = (NavierStokes.ParametricTorusInverse.Point → ℂ)

noncomputable def NavierStokes.ParametricTorusInverse.slice (f : Source) (p : ℝ) : TorusInverse.Plane → ℂ

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

Equations

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

def NavierStokes.ParametricTorusInverse.Periodic (f : Source) : Prop

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

Equations

• NavierStokes.ParametricTorusInverse.Periodic f = ∀ (p : ℝ), NavierStokes.SmoothFourierData.UnitPeriodic (NavierStokes.ParametricTorusInverse.slice f p)

noncomputable def NavierStokes.ParametricTorusInverse.parameterPartial (f : Source) (z : Point) : ℂ

Parameter partial, given by fderiv ℝ f z (1, 0).

Equations

• NavierStokes.ParametricTorusInverse.parameterPartial f z = (fderiv ℝ f z) (1, 0)

noncomputable def NavierStokes.ParametricTorusInverse.torusXPartial (f : Source) (z : Point) : ℂ

Torus X partial, given by fderiv ℝ f z (0, (1, 0)).

Equations

• NavierStokes.ParametricTorusInverse.torusXPartial f z = (fderiv ℝ f z) (0, 1, 0)

noncomputable def NavierStokes.ParametricTorusInverse.parameterJet (n : ℕ) (f : Source) : Source

Parameter jet, given by parameterPartial^[n] f.

Equations

• NavierStokes.ParametricTorusInverse.parameterJet n f = NavierStokes.ParametricTorusInverse.parameterPartial^[n] f

noncomputable def NavierStokes.ParametricTorusInverse.torusXJet : ℕ → Source → Source

Torus X jet as an element of ℕ → Source → Source | 0, f => f | n + 1, f => torusXPartial (torusXJet n f).

Equations

• NavierStokes.ParametricTorusInverse.torusXJet 0 x✝ = x✝
• NavierStokes.ParametricTorusInverse.torusXJet n.succ x✝ = NavierStokes.ParametricTorusInverse.torusXPartial (NavierStokes.ParametricTorusInverse.torusXJet n x✝)

noncomputable def NavierStokes.ParametricTorusInverse.swapTorus (f : Source) : Source

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

Equations

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

noncomputable def NavierStokes.ParametricTorusInverse.coefficient (f : Source) (p : ℝ) (k : TorusInverse.Frequency) : ℂ

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

Equations

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

noncomputable def NavierStokes.ParametricTorusInverse.mean (f : Source) (p : ℝ) : ℂ

Mean, given by coefficient f p 0.

Equations

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

def NavierStokes.ParametricTorusInverse.ZeroMean (f : Source) : Prop

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

Equations

• NavierStokes.ParametricTorusInverse.ZeroMean f = ∀ (p : ℝ), NavierStokes.ParametricTorusInverse.mean f p = 0

noncomputable def NavierStokes.ParametricTorusInverse.inverse (d : TorusInverse.Direction) (f : Source) (z : Point) : ℂ

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

Equations

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

noncomputable def NavierStokes.ParametricTorusInverse.iterateInverse (d : TorusInverse.Direction) (n : ℕ) (f : Source) : Source

Iterate inverse, given by (inverse d)^[n] f.

Equations

• NavierStokes.ParametricTorusInverse.iterateInverse d n f = (NavierStokes.ParametricTorusInverse.inverse d)^[n] f

theorem NavierStokes.ParametricTorusInverse.mean_eq_integral (f : Source) (p : ℝ) : mean f p = ∫ (y : ℝ) (x : ℝ) in 0..1, f (p, x, y)

theorem NavierStokes.ParametricTorusInverse.slice_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ) : ContDiff ℝ (↑⊤) (slice f p)

theorem NavierStokes.ParametricTorusInverse.fixedPartial_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (v : Point) : ContDiff ℝ ↑⊤ fun (z : Point) => (fderiv ℝ f z) v

theorem NavierStokes.ParametricTorusInverse.parameterPartial_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.torusXPartial_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (torusXPartial f)

theorem NavierStokes.ParametricTorusInverse.fixedPartial_periodic {f : Source} (hp : Periodic f) (v : Point) : Periodic fun (z : Point) => (fderiv ℝ f z) v

theorem NavierStokes.ParametricTorusInverse.parameterPartial_periodic {f : Source} (hp : Periodic f) : Periodic (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.torusXPartial_periodic {f : Source} (hp : Periodic f) : Periodic (torusXPartial f)

theorem NavierStokes.ParametricTorusInverse.torusXJet_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (torusXJet n f)

theorem NavierStokes.ParametricTorusInverse.parameterJet_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (parameterJet n f)

theorem NavierStokes.ParametricTorusInverse.parameterJet_periodic {f : Source} (hp : Periodic f) (n : ℕ) : Periodic (parameterJet n f)

theorem NavierStokes.ParametricTorusInverse.swapTorus_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (swapTorus f)

theorem NavierStokes.ParametricTorusInverse.parameter_slice_hasDerivAt {f : Source} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ) (Y : TorusInverse.Plane) : HasDerivAt (fun (q : ℝ) => f (q, Y)) (parameterPartial f (p, Y)) p

theorem NavierStokes.ParametricTorusInverse.slice_hasFDerivAt {f : Source} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ) (Y : TorusInverse.Plane) : HasFDerivAt (slice f p) (fderiv ℝ f (p, Y) ∘SL ContinuousLinearMap.inr ℝ ℝ TorusInverse.Plane) Y

theorem NavierStokes.ParametricTorusInverse.slice_torusXPartial {f : Source} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ) : slice (torusXPartial f) p = SmoothFourierData.partialX (slice f p)

theorem NavierStokes.ParametricTorusInverse.slice_torusXJet {f : Source} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (p : ℝ) : slice (torusXJet n f) p = SmoothFourierData.xJet n (slice f p)

theorem NavierStokes.ParametricTorusInverse.kernel_eq_mode (k : TorusInverse.Frequency) (Y : TorusInverse.Plane) : SmoothFourierData.kernel k Y = TorusInverse.mode (-k) Y

theorem NavierStokes.ParametricTorusInverse.mode_smooth (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (TorusInverse.mode k)

theorem NavierStokes.ParametricTorusInverse.kernel_smooth (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (SmoothFourierData.kernel k)

theorem NavierStokes.ParametricTorusInverse.integral_hasDerivAt {g g' : ℝ × ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g) (hd : ∀ (p u : ℝ), HasDerivAt (fun (q : ℝ) => g (q, u)) (g' (p, u)) p) (a b p : ℝ) : HasDerivAt (fun (q : ℝ) => ∫ (u : ℝ) in a..b, g (q, u)) (∫ (u : ℝ) in a..b, g' (p, u)) p

Differentiation of an actual fixed-interval integral.

noncomputable def NavierStokes.ParametricTorusInverse.weightedSource (k : TorusInverse.Frequency) (f : Source) (q : (ℝ × ℝ) × ℝ) : ℂ

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

Equations

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

theorem NavierStokes.ParametricTorusInverse.weightedSource_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) (weightedSource k f)

theorem NavierStokes.ParametricTorusInverse.coefficient_smooth {f : Source} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) : ContDiff ℝ ↑⊤ fun (p : ℝ) => coefficient f p k

theorem NavierStokes.ParametricTorusInverse.coefficient_hasDerivAt {f : Source} (hf : ContDiff ℝ (↑⊤) f) (k : TorusInverse.Frequency) (p : ℝ) : HasDerivAt (fun (q : ℝ) => coefficient f q k) (coefficient (parameterPartial f) p k) p

theorem NavierStokes.ParametricTorusInverse.parameterPartial_zeroMean {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hm : ZeroMean f) : ZeroMean (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.exists_uniform_coefficient_bound {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n : ℕ) (a b : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ Set.Icc a b, ∀ (k : TorusInverse.Frequency), TorusInverse.weight k ^ n * ‖coefficient f p k‖ ≤ C

Uniform polynomial decay on any fixed compact parameter interval, derived from bounds for actual torus derivatives.

def NavierStokes.ParametricTorusInverse.PolynomialGrowth (m : TorusInverse.Frequency → ℂ) : Prop

Polynomial growth, given by ∃ s : ℕ, ∃ C : ℝ, 0 ≤ C ∧ ∀ k, ‖m k‖ ≤ C * weight k ^ s.

Equations

• NavierStokes.ParametricTorusInverse.PolynomialGrowth m = ∃ (s : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ (k : NavierStokes.TorusInverse.Frequency), ‖m k‖ ≤ C * NavierStokes.TorusInverse.weight k ^ s

noncomputable def NavierStokes.ParametricTorusInverse.multiplierX (m : TorusInverse.Frequency → ℂ) (k : TorusInverse.Frequency) : ℂ

Multiplier X, given by freqX k * m k.

Equations

• NavierStokes.ParametricTorusInverse.multiplierX m k = NavierStokes.TorusInverse.freqX k * m k

noncomputable def NavierStokes.ParametricTorusInverse.multiplierY (m : TorusInverse.Frequency → ℂ) (k : TorusInverse.Frequency) : ℂ

Multiplier Y, given by freqY k * m k.

Equations

• NavierStokes.ParametricTorusInverse.multiplierY m k = NavierStokes.TorusInverse.freqY k * m k

theorem NavierStokes.ParametricTorusInverse.PolynomialGrowth.mulX {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) : PolynomialGrowth (multiplierX m)

theorem NavierStokes.ParametricTorusInverse.PolynomialGrowth.mulY {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) : PolynomialGrowth (multiplierY m)

theorem NavierStokes.ParametricTorusInverse.inverseMultiplier_growth (d : TorusInverse.Direction) : PolynomialGrowth (TorusInverse.multiplier d)

theorem NavierStokes.ParametricTorusInverse.PolynomialGrowth.rapid_mul {m a : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) (ha : TorusInverse.Rapid a) : TorusInverse.Rapid fun (k : TorusInverse.Frequency) => m k * a k

theorem NavierStokes.ParametricTorusInverse.multiplied_coeff_bound {m a : TorusInverse.Frequency → ℂ} {s : ℕ} {C B : ℝ} (hC : 0 ≤ C) (hm : ∀ (k : TorusInverse.Frequency), ‖m k‖ ≤ C * TorusInverse.weight k ^ s) (ha : ∀ (k : TorusInverse.Frequency), TorusInverse.weight k ^ (s + 4) * ‖a k‖ ≤ B) (k : TorusInverse.Frequency) : ‖m k * a k‖ ≤ C * B * (TorusInverse.weight k ^ 4)⁻¹

theorem NavierStokes.ParametricTorusInverse.uniform_multiplied_coeff_bound {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (a b : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ Set.Icc a b, ∀ (k : TorusInverse.Frequency), ‖m k * coefficient f p k‖ ≤ C * (TorusInverse.weight k ^ 4)⁻¹

noncomputable def NavierStokes.ParametricTorusInverse.applyMultiplier (m : TorusInverse.Frequency → ℂ) (f : Source) (z : Point) : ℂ

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.ParametricTorusInverse.inverse_eq_applyMultiplier (d : TorusInverse.Direction) (f : Source) : inverse d f = applyMultiplier (TorusInverse.multiplier d) f

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

noncomputable def NavierStokes.ParametricTorusInverse.jointDP : Point →L[ℝ] ℝ

Joint DP, given by ContinuousLinearMap.fst ℝ ℝ Plane.

Equations

• NavierStokes.ParametricTorusInverse.jointDP = ContinuousLinearMap.fst ℝ ℝ NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.ParametricTorusInverse.jointDX : Point →L[ℝ] ℝ

Joint DX, given by TorusInverse.dx.comp (ContinuousLinearMap.snd ℝ ℝ Plane).

Equations

• NavierStokes.ParametricTorusInverse.jointDX = NavierStokes.TorusInverse.dx ∘SL ContinuousLinearMap.snd ℝ ℝ NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.ParametricTorusInverse.jointDY : Point →L[ℝ] ℝ

Joint DY, given by TorusInverse.dy.comp (ContinuousLinearMap.snd ℝ ℝ Plane).

Equations

• NavierStokes.ParametricTorusInverse.jointDY = NavierStokes.TorusInverse.dy ∘SL ContinuousLinearMap.snd ℝ ℝ NavierStokes.TorusInverse.Plane

noncomputable def NavierStokes.ParametricTorusInverse.jointLiftP : ℂ →L[ℝ] Point →L[ℝ] ℂ

Joint lift P, given by ContinuousLinearMap.smulRightL ℝ Point ℂ jointDP.

Equations

• NavierStokes.ParametricTorusInverse.jointLiftP = (ContinuousLinearMap.smulRightL ℝ NavierStokes.ParametricTorusInverse.Point ℂ) NavierStokes.ParametricTorusInverse.jointDP

noncomputable def NavierStokes.ParametricTorusInverse.jointLiftX : ℂ →L[ℝ] Point →L[ℝ] ℂ

Joint lift X, given by ContinuousLinearMap.smulRightL ℝ Point ℂ jointDX.

Equations

• NavierStokes.ParametricTorusInverse.jointLiftX = (ContinuousLinearMap.smulRightL ℝ NavierStokes.ParametricTorusInverse.Point ℂ) NavierStokes.ParametricTorusInverse.jointDX

noncomputable def NavierStokes.ParametricTorusInverse.jointLiftY : ℂ →L[ℝ] Point →L[ℝ] ℂ

Joint lift Y, given by ContinuousLinearMap.smulRightL ℝ Point ℂ jointDY.

Equations

• NavierStokes.ParametricTorusInverse.jointLiftY = (ContinuousLinearMap.smulRightL ℝ NavierStokes.ParametricTorusInverse.Point ℂ) NavierStokes.ParametricTorusInverse.jointDY

@[simp]

theorem NavierStokes.ParametricTorusInverse.jointLiftP_apply (c : ℂ) (v : Point) : (jointLiftP c) v = v.1 • c

@[simp]

theorem NavierStokes.ParametricTorusInverse.jointLiftX_apply (c : ℂ) (v : Point) : (jointLiftX c) v = v.2.1 • c

@[simp]

theorem NavierStokes.ParametricTorusInverse.jointLiftY_apply (c : ℂ) (v : Point) : (jointLiftY c) v = v.2.2 • c

noncomputable def NavierStokes.ParametricTorusInverse.multiplierTermDerivative (m : TorusInverse.Frequency → ℂ) (f : Source) (k : TorusInverse.Frequency) (z : Point) : Point →L[ℝ] ℂ

Multiplier term derivative, constructed using jointLiftP.

Equations

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

theorem NavierStokes.ParametricTorusInverse.hasFDerivAt_multiplierTerm {f : Source} (hf : ContDiff ℝ (↑⊤) f) (m : TorusInverse.Frequency → ℂ) (k : TorusInverse.Frequency) (z : Point) : HasFDerivAt (fun (w : Point) => m k * coefficient f w.1 k * TorusInverse.mode k w.2) (multiplierTermDerivative m f k z) z

theorem NavierStokes.ParametricTorusInverse.norm_multiplierTermDerivative_le (m : TorusInverse.Frequency → ℂ) (f : Source) (k : TorusInverse.Frequency) (z : Point) : ‖multiplierTermDerivative m f k z‖ ≤ ‖jointLiftP‖ * ‖m k * coefficient (parameterPartial f) z.1 k‖ + ‖jointLiftX‖ * ‖multiplierX m k * coefficient f z.1 k‖ + ‖jointLiftY‖ * ‖multiplierY m k * coefficient f z.1 k‖

theorem NavierStokes.ParametricTorusInverse.uniform_multiplierDerivative_bound {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (a b : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : Point), z.1 ∈ Set.Icc a b → ∀ (k : TorusInverse.Frequency), ‖multiplierTermDerivative m f k z‖ ≤ C * (TorusInverse.weight k ^ 4)⁻¹

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

theorem NavierStokes.ParametricTorusInverse.fderiv_applyMultiplier {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (z : Point) : fderiv ℝ (applyMultiplier m f) z = jointLiftP (applyMultiplier m (parameterPartial f) z) + jointLiftX (applyMultiplier (multiplierX m) f z) + jointLiftY (applyMultiplier (multiplierY m) f z)

theorem NavierStokes.ParametricTorusInverse.applyMultiplier_smooth_nat (n : ℕ) {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑n) (applyMultiplier m f)

Joint smoothness is derived from actual locally uniform Fourier differentiation, allowing arbitrary polynomially growing multipliers.

theorem NavierStokes.ParametricTorusInverse.applyMultiplier_smooth {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑⊤) (applyMultiplier m f)

theorem NavierStokes.ParametricTorusInverse.inverse_smooth (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ContDiff ℝ (↑⊤) (inverse d f)

theorem NavierStokes.ParametricTorusInverse.parameterPartial_applyMultiplier {m : TorusInverse.Frequency → ℂ} (hm : PolynomialGrowth m) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : parameterPartial (applyMultiplier m f) = applyMultiplier m (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.parameterPartial_inverse (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : parameterPartial (inverse d f) = inverse d (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.inverse_periodic (d : TorusInverse.Direction) (f : Source) : Periodic (inverse d f)

theorem NavierStokes.ParametricTorusInverse.inverse_zeroMean (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) : ZeroMean (inverse d f)

The inverse has zero mean even if the input has a nonzero constant mode.

noncomputable def NavierStokes.ParametricTorusInverse.directionalPartial (d : TorusInverse.Direction) (f : Source) (z : Point) : ℂ

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

Equations

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

theorem NavierStokes.ParametricTorusInverse.inverse_solves (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (hm : ZeroMean f) : directionalPartial d (inverse d f) = f

Exact inversion for the given function, with the derivative taken in the joint parameter--torus space.

theorem NavierStokes.ParametricTorusInverse.inverse_preserves_parameter_support (d : TorusInverse.Direction) (f : Source) (S : Set ℝ) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (p : ℝ) : p ∉ S → ∀ (Y : TorusInverse.Plane), inverse d f (p, Y) = 0

@[simp]

theorem NavierStokes.ParametricTorusInverse.parameterJet_zero (f : Source) : parameterJet 0 f = f

theorem NavierStokes.ParametricTorusInverse.parameterJet_succ (n : ℕ) (f : Source) : parameterJet (n + 1) f = parameterPartial (parameterJet n f)

theorem NavierStokes.ParametricTorusInverse.parameterJet_zeroMean {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hm : ZeroMean f) (n : ℕ) : ZeroMean (parameterJet n f)

theorem NavierStokes.ParametricTorusInverse.parameterJet_inverse (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n : ℕ) : parameterJet n (inverse d f) = inverse d (parameterJet n f)

All actual derivatives in the external parameter commute with inversion.

@[simp]

theorem NavierStokes.ParametricTorusInverse.iterateInverse_zero (d : TorusInverse.Direction) (f : Source) : iterateInverse d 0 f = f

theorem NavierStokes.ParametricTorusInverse.iterateInverse_succ (d : TorusInverse.Direction) (n : ℕ) (f : Source) : iterateInverse d (n + 1) f = inverse d (iterateInverse d n f)

theorem NavierStokes.ParametricTorusInverse.iterateInverse_periodic (d : TorusInverse.Direction) {f : Source} (hp : Periodic f) (n : ℕ) : Periodic (iterateInverse d n f)

theorem NavierStokes.ParametricTorusInverse.iterateInverse_smooth (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n : ℕ) : ContDiff ℝ (↑⊤) (iterateInverse d n f)

theorem NavierStokes.ParametricTorusInverse.iterateInverse_zeroMean (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (hm : ZeroMean f) (n : ℕ) : ZeroMean (iterateInverse d n f)

theorem NavierStokes.ParametricTorusInverse.parameterPartial_iterateInverse (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n : ℕ) : parameterPartial (iterateInverse d n f) = iterateInverse d n (parameterPartial f)

theorem NavierStokes.ParametricTorusInverse.parameterJet_iterateInverse (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (n q : ℕ) : parameterJet q (iterateInverse d n f) = iterateInverse d n (parameterJet q f)

theorem NavierStokes.ParametricTorusInverse.iterateInverse_solves (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (hm : ZeroMean f) (n : ℕ) : directionalPartial d (iterateInverse d (n + 1) f) = iterateInverse d n f

theorem NavierStokes.ParametricTorusInverse.iterateInverse_preserves_parameter_support (d : TorusInverse.Direction) (f : Source) (S : Set ℝ) (hs : ∀ p ∉ S, ∀ (Y : TorusInverse.Plane), f (p, Y) = 0) (n : ℕ) (p : ℝ) : p ∉ S → ∀ (Y : TorusInverse.Plane), iterateInverse d n f (p, Y) = 0

noncomputable def NavierStokes.ParametricTorusInverse.mixedJet (q : ℕ) (w : List Bool) (f : Source) (z : Point) : ℂ

A genuine mixed coordinate jet: first actual parameter derivatives, then the indicated word of actual torus-coordinate derivatives.

Equations

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

noncomputable def NavierStokes.ParametricTorusInverse.mixedLossConstant (r : ℕ) : ℝ

Mixed loss constant, given by ((6 * ‖omega⁻¹‖) * ‖omega‖ ^ r) * 3 ^ (r + 5) * ∑' k : Frequency, (weight k ^ 4)⁻¹.

Equations

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

theorem NavierStokes.ParametricTorusInverse.mixedLossConstant_nonneg (r : ℕ) : 0 ≤ mixedLossConstant r

theorem NavierStokes.ParametricTorusInverse.mixedJet_inverse_bound (d : TorusInverse.Direction) {f : Source} (hf : ContDiff ℝ (↑⊤) f) (hp : Periodic f) (q : ℕ) (w : List Bool) (S : Set ℝ) {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, ‖SmoothFourierData.xJet (w.length + 5) (slice (parameterJet q f) p) (x, y)‖ ≤ C) (hsecond : ∀ p ∈ S, ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖SmoothFourierData.xJet (w.length + 5) (SmoothFourierData.swapFunction (slice (parameterJet q f) p)) (x, y)‖ ≤ C) (p : ℝ) (hps : p ∈ S) (Y : TorusInverse.Plane) : ‖mixedJet q w (inverse d f) (p, Y)‖ ≤ mixedLossConstant w.length * C

Uniform finite loss: a mixed output jet with r torus derivatives requires only r+5 pure torus derivatives of the same parameter jet of the input. The constant is independent of the parameter set and the function.