Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.SmoothFourierData

Fourier coefficients of actual smooth periodic functions #

Coefficients are defined by actual unit-interval integrals. Their decay is derived from integration by parts and bounds for actual coordinate derivatives.

Smooth Fourier series and directional inversion on the two-dimensional torus #

We work on the universal cover ℝ × ℝ, with frequencies in ℤ × ℤ. Rapid coefficients have summable polynomially weighted norms of every order.

Diophantine bounds for the manuscript's graph directions #

For every nonzero integer frequency (m,n), the directions v_r = (1, 1 - sqrt 2) and v_t = (sqrt 2 - 1, 1) have symbols bounded below by (1/6)/(1 + sqrt (m^2+n^2)). The proof multiplies each quadratic integer by its conjugate, proves that the resulting integer is nonzero using irrationality of sqrt 2, and bounds the conjugate explicitly.

noncomputable def NavierStokes.DiophantineGraph.quadraticForm (p q : ℤ) :

Quadratic form, given by (p : ℝ) + Real.sqrt 2 * (q : ℝ).

Equations

NavierStokes.DiophantineGraph.quadraticForm p q = ↑p + √2 * ↑q

Instances For

def NavierStokes.DiophantineGraph.integerNorm (p q : ℤ) :

Integer norm, given by p ^ 2 - 2 * q ^ 2.

Equations

NavierStokes.DiophantineGraph.integerNorm p q = p ^ 2 - 2 * q ^ 2

Instances For

theorem NavierStokes.DiophantineGraph.sqrt_two_square :

√2 ^ 2 = 2

theorem NavierStokes.DiophantineGraph.sqrt_two_le_two :

theorem NavierStokes.DiophantineGraph.quadraticForm_ne_zero (p q : ℤ) (hpq : p ≠ 0 ∨ q ≠ 0) :

quadraticForm p q ≠ 0

theorem NavierStokes.DiophantineGraph.conjugate_product (p q : ℤ) :

quadraticForm p q * quadraticForm p (-q) = ↑(integerNorm p q)

theorem NavierStokes.DiophantineGraph.integerNorm_ne_zero (p q : ℤ) (hpq : p ≠ 0 ∨ q ≠ 0) :

integerNorm p q ≠ 0

theorem NavierStokes.DiophantineGraph.conjugate_product_lower (p q : ℤ) (hpq : p ≠ 0 ∨ q ≠ 0) :

1 ≤ |quadraticForm p q| * |quadraticForm p (-q)|

The nonzero algebraic norm is an integer, so its absolute value is at least one.

noncomputable def NavierStokes.DiophantineGraph.radialSymbol (m n : ℤ) :

Radial symbol, given by quadraticForm (m + n) (-n).

Equations

NavierStokes.DiophantineGraph.radialSymbol m n = NavierStokes.DiophantineGraph.quadraticForm (m + n) (-n)

Instances For

noncomputable def NavierStokes.DiophantineGraph.timeSymbol (m n : ℤ) :

Time symbol, given by quadraticForm (n - m) m.

Equations

NavierStokes.DiophantineGraph.timeSymbol m n = NavierStokes.DiophantineGraph.quadraticForm (n - m) m

Instances For

noncomputable def NavierStokes.DiophantineGraph.radialConjugate (m n : ℤ) :

Radial conjugate, given by quadraticForm (m + n) n.

Equations

NavierStokes.DiophantineGraph.radialConjugate m n = NavierStokes.DiophantineGraph.quadraticForm (m + n) n

Instances For

noncomputable def NavierStokes.DiophantineGraph.timeConjugate (m n : ℤ) :

Time conjugate, given by quadraticForm (n - m) (-m).

Equations

NavierStokes.DiophantineGraph.timeConjugate m n = NavierStokes.DiophantineGraph.quadraticForm (n - m) (-m)

Instances For

theorem NavierStokes.DiophantineGraph.radialSymbol_formula (m n : ℤ) :

radialSymbol m n = ↑m + (1 - √2) * ↑n

theorem NavierStokes.DiophantineGraph.timeSymbol_formula (m n : ℤ) :

timeSymbol m n = (√2 - 1) * ↑m + ↑n

theorem NavierStokes.DiophantineGraph.radialConjugate_formula (m n : ℤ) :

radialConjugate m n = ↑m + (1 + √2) * ↑n

theorem NavierStokes.DiophantineGraph.timeConjugate_formula (m n : ℤ) :

timeConjugate m n = ↑n - (1 + √2) * ↑m

theorem NavierStokes.DiophantineGraph.radial_product_lower (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 ≤ |radialSymbol m n| * |radialConjugate m n|

theorem NavierStokes.DiophantineGraph.time_product_lower (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 ≤ |timeSymbol m n| * |timeConjugate m n|

def NavierStokes.DiophantineGraph.frequencyL1 (m n : ℤ) :

Frequency L1, given by |(m : ℝ)| + |(n : ℝ)|.

Equations

NavierStokes.DiophantineGraph.frequencyL1 m n = |↑m| + |↑n|

Instances For

noncomputable def NavierStokes.DiophantineGraph.frequencyLength (m n : ℤ) :

This is the usual Euclidean length of the integer frequency.

Equations

NavierStokes.DiophantineGraph.frequencyLength m n = √(↑m ^ 2 + ↑n ^ 2)

Instances For

theorem NavierStokes.DiophantineGraph.frequencyL1_nonneg (m n : ℤ) :

0 ≤ frequencyL1 m n

theorem NavierStokes.DiophantineGraph.frequencyLength_nonneg (m n : ℤ) :

0 ≤ frequencyLength m n

theorem NavierStokes.DiophantineGraph.radialConjugate_upper (m n : ℤ) :

|radialConjugate m n| ≤ 3 * frequencyL1 m n

theorem NavierStokes.DiophantineGraph.timeConjugate_upper (m n : ℤ) :

|timeConjugate m n| ≤ 3 * frequencyL1 m n

theorem NavierStokes.DiophantineGraph.frequencyL1_le_twice_length (m n : ℤ) :

frequencyL1 m n ≤ 2 * frequencyLength m n

theorem NavierStokes.DiophantineGraph.lower_of_conjugate_bound {a b D : ℝ} (hprod : 1 ≤ |a| * |b|) (hD : 0 < D) (hb : |b| ≤ D) :

1 / D ≤ |a|

theorem NavierStokes.DiophantineGraph.radial_diophantine_l1 (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 / 3 / (1 + frequencyL1 m n) ≤ |radialSymbol m n|

Explicit Diophantine bound for v_r = (1,1-sqrt 2) in the L1 length.

theorem NavierStokes.DiophantineGraph.time_diophantine_l1 (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 / 3 / (1 + frequencyL1 m n) ≤ |timeSymbol m n|

Explicit Diophantine bound for v_t = (sqrt 2-1,1) in the L1 length.

theorem NavierStokes.DiophantineGraph.radial_diophantine (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 / 6 / (1 + frequencyLength m n) ≤ |radialSymbol m n|

The manuscript's estimate with an explicit constant and Euclidean length.

theorem NavierStokes.DiophantineGraph.time_diophantine (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

1 / 6 / (1 + frequencyLength m n) ≤ |timeSymbol m n|

The manuscript's estimate for the second graph direction.

theorem NavierStokes.DiophantineGraph.radialSymbol_ne_zero (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

radialSymbol m n ≠ 0

theorem NavierStokes.DiophantineGraph.timeSymbol_ne_zero (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

timeSymbol m n ≠ 0

theorem NavierStokes.DiophantineGraph.radial_reciprocal_bound (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

|1 / radialSymbol m n| ≤ 6 * (1 + frequencyLength m n)

The radial inverse Fourier multiplier grows at most linearly in frequency.

theorem NavierStokes.DiophantineGraph.time_reciprocal_bound (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) :

|1 / timeSymbol m n| ≤ 6 * (1 + frequencyLength m n)

The temporal inverse Fourier multiplier grows at most linearly in frequency.

theorem NavierStokes.DiophantineGraph.radial_inverse_power_bound (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) (p : ℕ) :

|1 / radialSymbol m n| ^ p ≤ (6 * (1 + frequencyLength m n)) ^ p

Repeated radial inversion has the corresponding finite polynomial loss.

theorem NavierStokes.DiophantineGraph.time_inverse_power_bound (m n : ℤ) (hmn : m ≠ 0 ∨ n ≠ 0) (p : ℕ) :

|1 / timeSymbol m n| ^ p ≤ (6 * (1 + frequencyLength m n)) ^ p

Repeated temporal inversion has the corresponding finite polynomial loss.

theorem NavierStokes.DiophantineGraph.graph_directions_diophantine (k : ℤ × ℤ) (hk : k ≠ 0) :

1 / 6 / (1 + frequencyLength k.1 k.2) ≤ |↑k.1 + (1 - √2) * ↑k.2| ∧ 1 / 6 / (1 + frequencyLength k.1 k.2) ≤ |(√2 - 1) * ↑k.1 + ↑k.2|

Both estimates packaged for a nonzero integer vector.

def NavierStokes.DiophantineGraph.coveringFrequency (k : ℤ × ℤ) :

The integer matrix [[3,1],[1,5]] acting on a frequency.

Equations

NavierStokes.DiophantineGraph.coveringFrequency k = (3 * k.1 + k.2, k.1 + 5 * k.2)

Instances For

theorem NavierStokes.DiophantineGraph.coveringFrequency_injective :

Function.Injective coveringFrequency

theorem NavierStokes.DiophantineGraph.coveringFrequency_ne_zero (k : ℤ × ℤ) (hk : k ≠ 0) :

coveringFrequency k ≠ 0

theorem NavierStokes.DiophantineGraph.radial_symbol_covering (k : ℤ × ℤ) :

radialSymbol (coveringFrequency k).1 (coveringFrequency k).2 = (4 - √2) * radialSymbol k.1 k.2

The radial symbol scales by the smaller eigenvalue of the covering matrix.

theorem NavierStokes.DiophantineGraph.time_symbol_covering (k : ℤ × ℤ) :

timeSymbol (coveringFrequency k).1 (coveringFrequency k).2 = (4 + √2) * timeSymbol k.1 k.2

The temporal symbol scales by the larger eigenvalue of the covering matrix.

theorem NavierStokes.DiophantineGraph.covering_eigenvalues_gt_one :

1 < 4 - √2 ∧ 1 < 4 + √2

@[reducible, inline]

abbrev NavierStokes.TorusInverse.Frequency :

Frequency: an abbreviation for ℤ × ℤ.

Equations

NavierStokes.TorusInverse.Frequency = (ℤ × ℤ)

Instances For

@[reducible, inline]

abbrev NavierStokes.TorusInverse.Plane :

Plane: an abbreviation for ℝ × ℝ.

Equations

NavierStokes.TorusInverse.Plane = (ℝ × ℝ)

Instances For

def NavierStokes.TorusInverse.weight (k : Frequency) :

Weight, given by 1 + |(k.1 : ℝ)| + |(k.2 : ℝ)|.

Equations

NavierStokes.TorusInverse.weight k = 1 + |↑k.1| + |↑k.2|

Instances For

theorem NavierStokes.TorusInverse.weight_pos (k : Frequency) :

def NavierStokes.TorusInverse.Rapid (a : Frequency → ℂ) :

Polynomially weighted absolute summability of every order.

Equations

NavierStokes.TorusInverse.Rapid a = ∀ (p : ℕ), Summable fun (k : NavierStokes.TorusInverse.Frequency) => NavierStokes.TorusInverse.weight k ^ p * ‖a k‖

Instances For

theorem NavierStokes.TorusInverse.Rapid.summable_norm {a : Frequency → ℂ} (ha : Rapid a) :

Summable fun (k : Frequency) => ‖a k‖

theorem NavierStokes.TorusInverse.Rapid.mul_linear {a b : Frequency → ℂ} (ha : Rapid a) (C : ℝ) (hb : ∀ (k : Frequency), ‖b k‖ ≤ C * weight k) :

Rapid fun (k : Frequency) => b k * a k

noncomputable def NavierStokes.TorusInverse.omega :

Omega, given by 2 * Real.pi * Complex.I.

Equations

NavierStokes.TorusInverse.omega = 2 * ↑Real.pi * Complex.I

Instances For

noncomputable def NavierStokes.TorusInverse.freqX (k : Frequency) :

Freq X, given by omega * (k.1 : ℂ).

Equations

NavierStokes.TorusInverse.freqX k = NavierStokes.TorusInverse.omega * ↑k.1

Instances For

noncomputable def NavierStokes.TorusInverse.freqY (k : Frequency) :

Freq Y, given by omega * (k.2 : ℂ).

Equations

NavierStokes.TorusInverse.freqY k = NavierStokes.TorusInverse.omega * ↑k.2

Instances For

def NavierStokes.TorusInverse.dx :

Plane →L[ℝ ] ℝ

Dx, given by ContinuousLinearMap.fst ℝ ℝ ℝ.

Equations

NavierStokes.TorusInverse.dx = ContinuousLinearMap.fst ℝ ℝ ℝ

Instances For

def NavierStokes.TorusInverse.dy :

Plane →L[ℝ ] ℝ

Dy, given by ContinuousLinearMap.snd ℝ ℝ ℝ.

Equations

NavierStokes.TorusInverse.dy = ContinuousLinearMap.snd ℝ ℝ ℝ

Instances For

noncomputable def NavierStokes.TorusInverse.liftX :

ℂ →L[ℝ ] Plane →L[ℝ ] ℂ

Lift X, given by ContinuousLinearMap.smulRightL ℝ Plane ℂ dx.

Equations

NavierStokes.TorusInverse.liftX = (ContinuousLinearMap.smulRightL ℝ NavierStokes.TorusInverse.Plane ℂ) NavierStokes.TorusInverse.dx

Instances For

noncomputable def NavierStokes.TorusInverse.liftY :

ℂ →L[ℝ ] Plane →L[ℝ ] ℂ

Lift Y, given by ContinuousLinearMap.smulRightL ℝ Plane ℂ dy.

Equations

NavierStokes.TorusInverse.liftY = (ContinuousLinearMap.smulRightL ℝ NavierStokes.TorusInverse.Plane ℂ) NavierStokes.TorusInverse.dy

Instances For

@[simp]

theorem NavierStokes.TorusInverse.liftX_apply (c : ℂ) (x : Plane) :

(liftX c) x = x.1 • c

@[simp]

theorem NavierStokes.TorusInverse.liftY_apply (c : ℂ) (x : Plane) :

(liftY c) x = x.2 • c

noncomputable def NavierStokes.TorusInverse.phase (k : Frequency) :

Plane →L[ℝ ] ℂ

Phase, given by liftX (freqX k) + liftY (freqY k).

Equations

NavierStokes.TorusInverse.phase k = NavierStokes.TorusInverse.liftX (NavierStokes.TorusInverse.freqX k) + NavierStokes.TorusInverse.liftY (NavierStokes.TorusInverse.freqY k)

Instances For

noncomputable def NavierStokes.TorusInverse.mode (k : Frequency) (x : Plane) :

Mode, given by Complex.exp (phase k x).

Equations

NavierStokes.TorusInverse.mode k x = Complex.exp ((NavierStokes.TorusInverse.phase k) x)

Instances For

theorem NavierStokes.TorusInverse.phase_formula (k : Frequency) (x : Plane) :

(phase k) x = omega * (↑k.1 * ↑x.1 + ↑k.2 * ↑x.2)

theorem NavierStokes.TorusInverse.norm_mode (k : Frequency) (x : Plane) :

‖mode k x‖ = 1

theorem NavierStokes.TorusInverse.continuous_mode (k : Frequency) :

Continuous (mode k)

noncomputable def NavierStokes.TorusInverse.derivX (a : Frequency → ℂ) (k : Frequency) :

Deriv X, given by freqX k * a k.

Equations

NavierStokes.TorusInverse.derivX a k = NavierStokes.TorusInverse.freqX k * a k

Instances For

noncomputable def NavierStokes.TorusInverse.derivY (a : Frequency → ℂ) (k : Frequency) :

Deriv Y, given by freqY k * a k.

Equations

NavierStokes.TorusInverse.derivY a k = NavierStokes.TorusInverse.freqY k * a k

Instances For

theorem NavierStokes.TorusInverse.norm_freqX_le (k : Frequency) :

‖freqX k‖ ≤ ‖omega ‖ * weight k

theorem NavierStokes.TorusInverse.norm_freqY_le (k : Frequency) :

‖freqY k‖ ≤ ‖omega ‖ * weight k

theorem NavierStokes.TorusInverse.Rapid.derivX {a : Frequency → ℂ} (ha : Rapid a) :

Rapid (TorusInverse.derivX a)

theorem NavierStokes.TorusInverse.Rapid.derivY {a : Frequency → ℂ} (ha : Rapid a) :

Rapid (TorusInverse.derivY a)

noncomputable def NavierStokes.TorusInverse.series (a : Frequency → ℂ) (x : Plane) :

Series, given by ∑' k, a k * mode k x.

Equations

NavierStokes.TorusInverse.series a x = ∑' (k : NavierStokes.TorusInverse.Frequency), a k * NavierStokes.TorusInverse.mode k x

Instances For

theorem NavierStokes.TorusInverse.summable_terms {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

Summable fun (k : Frequency) => a k * mode k x

theorem NavierStokes.TorusInverse.continuous_series {a : Frequency → ℂ} (ha : Rapid a) :

Continuous (series a)

noncomputable def NavierStokes.TorusInverse.termDeriv (a : Frequency → ℂ) (k : Frequency) (x : Plane) :

Plane →L[ℝ ] ℂ

Term derivative, given by liftX (derivX a k * mode k x) + liftY (derivY a k * mode k x).

Equations

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

Instances For

theorem NavierStokes.TorusInverse.hasFDerivAt_term (a : Frequency → ℂ) (k : Frequency) (x : Plane) :

HasFDerivAt (fun (y : Plane) => a k * mode k y) (termDeriv a k x) x

noncomputable def NavierStokes.TorusInverse.derivativeMajorant (a : Frequency → ℂ) (k : Frequency) :

Derivative majorant, given by ‖liftX‖ * ‖derivX a k‖ + ‖liftY‖ * ‖derivY a k‖.

Equations

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

Instances For

theorem NavierStokes.TorusInverse.summable_derivativeMajorant {a : Frequency → ℂ} (ha : Rapid a) :

Summable (derivativeMajorant a)

theorem NavierStokes.TorusInverse.norm_termDeriv_le (a : Frequency → ℂ) (k : Frequency) (x : Plane) :

‖termDeriv a k x‖ ≤ derivativeMajorant a k

theorem NavierStokes.TorusInverse.summable_termDeriv {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

Summable fun (k : Frequency) => termDeriv a k x

theorem NavierStokes.TorusInverse.hasFDerivAt_series {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

HasFDerivAt (series a) (∑' (k : Frequency), termDeriv a k x) x

theorem NavierStokes.TorusInverse.fderiv_series {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

fderiv ℝ (series a) x = liftX (series (derivX a) x) + liftY (series (derivY a) x)

theorem NavierStokes.TorusInverse.contDiff_series_nat (p : ℕ) {a : Frequency → ℂ} (ha : Rapid a) :

ContDiff ℝ (↑p) (series a)

Smoothness is proved from summability and termwise differentiation.

theorem NavierStokes.TorusInverse.contDiff_series {a : Frequency → ℂ} (ha : Rapid a) :

ContDiff ℝ (↑⊤) (series a)

inductive NavierStokes.TorusInverse.Direction :

Direction data for torus inverse.

radial : Direction
temporal : Direction

Instances For

@[instance_reducible]

instance NavierStokes.TorusInverse.instDecidableEqDirection :

DecidableEq Direction

Equations

NavierStokes.TorusInverse.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

noncomputable def NavierStokes.TorusInverse.vector :

Direction → Plane

Vector as an element of Direction → Plane | .radial => (1, 1 - Real.sqrt 2) | .temporal => (Real.sqrt 2 - 1, 1).

Equations

Instances For

noncomputable def NavierStokes.TorusInverse.symbol :

Direction → Frequency → ℝ

Symbol as an element of Direction → Frequency → ℝ | .radial, k => DiophantineGraph.radialSymbol k.1 k.2 | .temporal, k => DiophantineGraph.timeSymbol k.1 k.2.

Equations

NavierStokes.TorusInverse.symbol NavierStokes.TorusInverse.Direction.radial x✝ = NavierStokes.DiophantineGraph.radialSymbol x✝.1 x✝.2
NavierStokes.TorusInverse.symbol NavierStokes.TorusInverse.Direction.temporal x✝ = NavierStokes.DiophantineGraph.timeSymbol x✝.1 x✝.2

Instances For

theorem NavierStokes.TorusInverse.pair_nonzero {k : Frequency} (hk : k ≠ 0) :

k.1 ≠ 0 ∨ k.2 ≠ 0

theorem NavierStokes.TorusInverse.symbol_formula (d : Direction) (k : Frequency) :

symbol d k = ↑k.1 * (vector d).1 + ↑k.2 * (vector d).2

theorem NavierStokes.TorusInverse.symbol_ne_zero (d : Direction) {k : Frequency} (hk : k ≠ 0) :

symbol d k ≠ 0

theorem NavierStokes.TorusInverse.length_le_weight (k : Frequency) :

1 + DiophantineGraph.frequencyLength k.1 k.2 ≤ weight k

theorem NavierStokes.TorusInverse.reciprocal_symbol_bound (d : Direction) {k : Frequency} (hk : k ≠ 0) :

|1 / symbol d k| ≤ 6 * weight k

theorem NavierStokes.TorusInverse.omega_ne_zero :

noncomputable def NavierStokes.TorusInverse.multiplier (d : Direction) (k : Frequency) :

Multiplier, given by (omega * (symbol d k : ℂ))⁻¹.

Equations

NavierStokes.TorusInverse.multiplier d k = (NavierStokes.TorusInverse.omega * ↑(NavierStokes.TorusInverse.symbol d k))⁻¹

Instances For

noncomputable def NavierStokes.TorusInverse.inverseCoeff (d : Direction) (a : Frequency → ℂ) (k : Frequency) :

Inverse coefficient, given by multiplier d k * a k.

Equations

NavierStokes.TorusInverse.inverseCoeff d a k = NavierStokes.TorusInverse.multiplier d k * a k

Instances For

@[simp]

theorem NavierStokes.TorusInverse.symbol_zero (d : Direction) :

symbol d 0 = 0

@[simp]

theorem NavierStokes.TorusInverse.inverseCoeff_zero (d : Direction) (a : Frequency → ℂ) :

inverseCoeff d a 0 = 0

theorem NavierStokes.TorusInverse.norm_multiplier_le (d : Direction) (k : Frequency) :

‖multiplier d k‖ ≤ 6 * ‖omega ⁻¹ ‖ * weight k

theorem NavierStokes.TorusInverse.Rapid.inverseCoeff {a : Frequency → ℂ} (ha : Rapid a) (d : Direction) :

Rapid (TorusInverse.inverseCoeff d a)

theorem NavierStokes.TorusInverse.inverseCoeff_weighted_bound (d : Direction) (a : Frequency → ℂ) (p : ℕ) (k : Frequency) :

weight k ^ p * ‖inverseCoeff d a k‖ ≤ 6 * ‖omega ⁻¹ ‖ * (weight k ^ (p + 1) * ‖a k‖)

The coefficient estimate loses one polynomial frequency weight.

theorem NavierStokes.TorusInverse.coefficient_cancel (d : Direction) {a : Frequency → ℂ} (hzero : a 0 = 0) (k : Frequency) :

omega * ↑(symbol d k) * inverseCoeff d a k = a k

noncomputable def NavierStokes.TorusInverse.directionalInverse (d : Direction) (a : Frequency → ℂ) :

Directional inverse, given by series (inverseCoeff d a).

Equations

NavierStokes.TorusInverse.directionalInverse d a = NavierStokes.TorusInverse.series (NavierStokes.TorusInverse.inverseCoeff d a)

Instances For

theorem NavierStokes.TorusInverse.contDiff_directionalInverse (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) :

ContDiff ℝ (↑⊤) (directionalInverse d a)

theorem NavierStokes.TorusInverse.termDeriv_direction (d : Direction) {a : Frequency → ℂ} (hzero : a 0 = 0) (k : Frequency) (x : Plane) :

(termDeriv (inverseCoeff d a) k x) (vector d) = a k * mode k x

theorem NavierStokes.TorusInverse.directionalInverse_solves (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) (hzero : a 0 = 0) (x : Plane) :

(fderiv ℝ (directionalInverse d a) x) (vector d) = series a x

The genuine Fréchet derivative of the smooth inverse solves the equation.

Descent to the torus and actual Haar means #

theorem NavierStokes.TorusInverse.instTorusInverse1 :

Fact (0 < 1)

@[reducible, inline]

abbrev NavierStokes.TorusInverse.Torus :

Torus: an abbreviation for UnitAddCircle × UnitAddCircle.

Equations

NavierStokes.TorusInverse.Torus = (UnitAddCircle × UnitAddCircle)

Instances For

noncomputable def NavierStokes.TorusInverse.torusMeasure :

MeasureTheory.Measure Torus

Torus measure as an element of Measure Torus.

Equations

NavierStokes.TorusInverse.torusMeasure = AddCircle.haarAddCircle.prod AddCircle.haarAddCircle

Instances For

instance NavierStokes.TorusInverse.instIsProbabilityMeasureTorusTorusMeasure :

MeasureTheory.IsProbabilityMeasure torusMeasure

noncomputable def NavierStokes.TorusInverse.torusMode (k : Frequency) :

C(Torus , ℂ )

Torus mode, bundling toFun, continuous_toFun.

Equations

NavierStokes.TorusInverse.torusMode k = { toFun := fun (z : NavierStokes.TorusInverse.Torus) => (fourier k.1) z.1 * (fourier k.2) z.2, continuous_toFun := ⋯ }

Instances For

theorem NavierStokes.TorusInverse.norm_torusMode (k : Frequency) (z : Torus) :

‖(torusMode k) z‖ = 1

noncomputable def NavierStokes.TorusInverse.torusSeries (a : Frequency → ℂ) (z : Torus) :

Torus series, given by ∑' k, a k * torusMode k z.

Equations

NavierStokes.TorusInverse.torusSeries a z = ∑' (k : NavierStokes.TorusInverse.Frequency), a k * (NavierStokes.TorusInverse.torusMode k) z

Instances For

theorem NavierStokes.TorusInverse.mode_eq_torusMode (k : Frequency) (x : Plane) :

mode k x = (torusMode k) (↑x.1, ↑x.2)

theorem NavierStokes.TorusInverse.series_eq_torusSeries (a : Frequency → ℂ) (x : Plane) :

series a x = torusSeries a (↑x.1, ↑x.2)

theorem NavierStokes.TorusInverse.circle_int_eq_zero (m : ℤ) :

↑↑m = 0

theorem NavierStokes.TorusInverse.series_periodic (a : Frequency → ℂ) (x : Plane) (m n : ℤ) :

series a (x.1 + ↑m, x.2 + ↑n) = series a x

Integer translation invariance is actual descent to (ℝ/ℤ)².

theorem NavierStokes.TorusInverse.continuous_torusSeries {a : Frequency → ℂ} (ha : Rapid a) :

Continuous (torusSeries a)

theorem NavierStokes.TorusInverse.integral_fourier (n : ℤ) :

∫ (z : UnitAddCircle), (fourier n) z ∂AddCircle.haarAddCircle = if n = 0 then 1 else 0

theorem NavierStokes.TorusInverse.integral_torusMode (k : Frequency) :

∫ (z : Torus), (torusMode k) z ∂torusMeasure = if k = 0 then 1 else 0

theorem NavierStokes.TorusInverse.integrable_torusTerm (a : Frequency → ℂ) (k : Frequency) :

MeasureTheory.Integrable (fun (z : Torus) => a k * (torusMode k) z) torusMeasure

theorem NavierStokes.TorusInverse.integral_torusSeries {a : Frequency → ℂ} (ha : Rapid a) :

∫ (z : Torus), torusSeries a z ∂torusMeasure = a 0

The zeroth coefficient equals the actual normalized Haar integral.

noncomputable def NavierStokes.TorusInverse.coeffSeminorm (p : ℕ) (a : Frequency → ℂ) :

Weighted absolute Fourier coefficient seminorm.

Equations

NavierStokes.TorusInverse.coeffSeminorm p a = ∑' (k : NavierStokes.TorusInverse.Frequency), NavierStokes.TorusInverse.weight k ^ p * ‖a k‖

Instances For

theorem NavierStokes.TorusInverse.inverseCoeff_seminorm_le (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) (p : ℕ) :

coeffSeminorm p (inverseCoeff d a) ≤ 6 * ‖omega ⁻¹ ‖ * coeffSeminorm (p + 1) a

theorem NavierStokes.TorusInverse.norm_series_le {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

‖series a x‖ ≤ coeffSeminorm 0 a

theorem NavierStokes.TorusInverse.norm_directionalInverse_le (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) (x : Plane) :

‖directionalInverse d a x‖ ≤ 6 * ‖omega ⁻¹ ‖ * coeffSeminorm 1 a

noncomputable def NavierStokes.TorusInverse.coordinateCoeff (j : Bool) (a : Frequency → ℂ) :

Frequency → ℂ

Coordinate coefficient, with branches according to j.

Equations

NavierStokes.TorusInverse.coordinateCoeff j a = if j = true then NavierStokes.TorusInverse.derivY a else NavierStokes.TorusInverse.derivX a

Instances For

noncomputable def NavierStokes.TorusInverse.coordinatePartial (j : Bool) (f : Plane → ℂ) (x : Plane) :

Coordinate partial, given by fderiv ℝ f x (if j then (0, 1) else (1, 0)).

Equations

NavierStokes.TorusInverse.coordinatePartial j f x = (fderiv ℝ f x) (if j = true then (0, 1) else (1, 0))

Instances For

def NavierStokes.TorusInverse.coefficientWord :

List Bool → (Frequency → ℂ) → Frequency → ℂ

Coefficient word as an element of js, a => coordinateCoeff j (coefficientWord js a).

Equations

NavierStokes.TorusInverse.coefficientWord [] x✝ = x✝
NavierStokes.TorusInverse.coefficientWord (j :: js) x✝ = NavierStokes.TorusInverse.coordinateCoeff j (NavierStokes.TorusInverse.coefficientWord js x✝)

Instances For

def NavierStokes.TorusInverse.derivativeWord :

List Bool → (Plane → ℂ) → Plane → ℂ

Derivative word as an element of js, f => coordinatePartial j (derivativeWord js f).

Equations

NavierStokes.TorusInverse.derivativeWord [] x✝ = x✝
NavierStokes.TorusInverse.derivativeWord (j :: js) x✝ = NavierStokes.TorusInverse.coordinatePartial j (NavierStokes.TorusInverse.derivativeWord js x✝)

Instances For

theorem NavierStokes.TorusInverse.Rapid.coordinateCoeff {a : Frequency → ℂ} (ha : Rapid a) (j : Bool) :

Rapid (TorusInverse.coordinateCoeff j a)

theorem NavierStokes.TorusInverse.Rapid.coefficientWord {a : Frequency → ℂ} (ha : Rapid a) (w : List Bool) :

Rapid (TorusInverse.coefficientWord w a)

theorem NavierStokes.TorusInverse.coordinatePartial_series (j : Bool) {a : Frequency → ℂ} (ha : Rapid a) :

coordinatePartial j (series a) = series (coordinateCoeff j a)

theorem NavierStokes.TorusInverse.derivativeWord_series (w : List Bool) {a : Frequency → ℂ} (ha : Rapid a) :

derivativeWord w (series a) = series (coefficientWord w a)

theorem NavierStokes.TorusInverse.norm_coordinateCoeff_le (j : Bool) (a : Frequency → ℂ) (k : Frequency) :

‖coordinateCoeff j a k‖ ≤ ‖omega ‖ * weight k * ‖a k‖

theorem NavierStokes.TorusInverse.norm_coefficientWord_le (w : List Bool) (a : Frequency → ℂ) (k : Frequency) :

‖coefficientWord w a k‖ ≤ (‖omega ‖ * weight k) ^ w.length * ‖a k‖

theorem NavierStokes.TorusInverse.inverse_derivativeWord_bound (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) (w : List Bool) (x : Plane) :

‖derivativeWord w (directionalInverse d a) x‖ ≤ 6 * ‖omega ⁻¹ ‖ * ‖omega ‖ ^ w.length * coeffSeminorm (w.length + 1) a

A uniform bound for every actual mixed coordinate derivative of the inverse.

Parameters and support #

theorem NavierStokes.TorusInverse.hasDerivAt_parameter_series (a a' : ℝ → Frequency → ℂ) (B : Frequency → ℝ) (hderiv : ∀ (k : Frequency) (t : ℝ), HasDerivAt (fun (s : ℝ) => a s k) (a' t k) t) (hB : Summable B) (hbound : ∀ (k : Frequency) (t : ℝ), ‖a' t k‖ ≤ B k) (t₀ : ℝ) (hinit : Rapid (a t₀)) (x : Plane) (t : ℝ) :

HasDerivAt (fun (s : ℝ) => series (a s) x) (series (a' t) x) t

theorem NavierStokes.TorusInverse.hasDerivAt_parameter_inverse (d : Direction) (a a' : ℝ → Frequency → ℂ) (B : Frequency → ℝ) (hderiv : ∀ (k : Frequency) (t : ℝ), HasDerivAt (fun (s : ℝ) => a s k) (a' t k) t) (hB : Summable fun (k : Frequency) => weight k * B k) (hbound : ∀ (k : Frequency) (t : ℝ), ‖a' t k‖ ≤ B k) (t₀ : ℝ) (hinit : Rapid (a t₀)) (x : Plane) (t : ℝ) :

HasDerivAt (fun (s : ℝ) => directionalInverse d (a s) x) (directionalInverse d (a' t) x) t

Parameter differentiation commutes with the actual inverse series under a uniform summable bound on one frequency-weighted parameter derivative.

theorem NavierStokes.TorusInverse.inverse_preserves_parameter_support {P : Type u_1} (d : Direction) (a : P → Frequency → ℂ) (S : Set P) (hsupport : ∀ p ∉ S, ∀ (k : Frequency), a p k = 0) (p : P) :

p ∉ S → ∀ (x : Plane), directionalInverse d (a p) x = 0

Inversion uses only the torus variable and preserves support in every external parameter. No nonvanishing or convergence hypothesis is needed here.

theorem NavierStokes.TorusInverse.inverse_zero_mean (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) :

∫ (z : Torus), torusSeries (inverseCoeff d a) z ∂torusMeasure = 0

The constructed directional inverse has zero normalized Haar mean.

theorem NavierStokes.TorusInverse.directionalInverse_periodic (d : Direction) (a : Frequency → ℂ) (x : Plane) (m n : ℤ) :

directionalInverse d a (x.1 + ↑m, x.2 + ↑n) = directionalInverse d a x

theorem NavierStokes.TorusInverse.zero_mean_series_has_smooth_inverse (d : Direction) {a : Frequency → ℂ} (ha : Rapid a) (hmean : ∫ (z : Torus), torusSeries a z ∂torusMeasure = 0) :

∃ (u : Torus → ℂ), Continuous u ∧ ∫ (z : Torus), u z ∂torusMeasure = 0 ∧ (ContDiff ℝ ↑⊤ fun (x : Plane) => u (↑x.1, ↑x.2)) ∧ ∀ (x : Plane), (fderiv ℝ (fun (y : Plane) => u (↑y.1, ↑y.2)) x) (vector d) = series a x

A zero-average rapidly convergent Fourier series on the actual torus has a zero-average inverse whose universal-cover lift is smooth and solves the directional equation. Both manuscript directions are covered.

theorem NavierStokes.SmoothFourierData.instSmoothFourierData1 :

Fact (0 < 1)

noncomputable def NavierStokes.SmoothFourierData.unitCoeff (f : ℝ → ℂ) (n : ℤ) :

The actual unit-period Fourier coefficient of a function on the line.

Equations

NavierStokes.SmoothFourierData.unitCoeff f n = fourierCoeffOn NavierStokes.SmoothFourierData.unitCoeff._proof_1 f n

Instances For

theorem NavierStokes.SmoothFourierData.unitCoeff_eq_integral (f : ℝ → ℂ) (n : ℤ) :

unitCoeff f n = ∫ (x : ℝ) in 0..1, (fourier (-n)) ↑x * f x

theorem NavierStokes.SmoothFourierData.unitCoeff_const_mul (f : ℝ → ℂ) (c : ℂ) (n : ℤ) :

unitCoeff (fun (x : ℝ) => c * f x) n = c * unitCoeff f n

theorem NavierStokes.SmoothFourierData.unitCoeff_norm_le {f : ℝ → ℂ} {C : ℝ} (n : ℤ) (hb : ∀ x ∈ Set.Icc 0 1, ‖f x‖ ≤ C) :

‖unitCoeff f n‖ ≤ C

theorem NavierStokes.SmoothFourierData.unitCoeff_of_hasDerivAt {f f' : ℝ → ℂ} {n : ℤ} (hn : n ≠ 0) (hd : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hc : Continuous f') (hp : f 1 = f 0) :

unitCoeff f n = (TorusInverse.omega * ↑n)⁻¹ * unitCoeff f' n

The boundary term cancels because the actual endpoint values agree.

def NavierStokes.SmoothFourierData.UnitPeriodic (f : TorusInverse.Plane → ℂ) :

Unit-periodicity in both coordinates, expressed on the universal cover.

Equations

NavierStokes.SmoothFourierData.UnitPeriodic f = ∀ (z : NavierStokes.TorusInverse.Plane) (k : NavierStokes.TorusInverse.Frequency), f (z + (↑k.1, ↑k.2)) = f z

Instances For

noncomputable def NavierStokes.SmoothFourierData.partialX (f : TorusInverse.Plane → ℂ) (z : TorusInverse.Plane) :

The genuine first coordinate derivative.

Equations

NavierStokes.SmoothFourierData.partialX f z = (fderiv ℝ f z) (1, 0)

Instances For

noncomputable def NavierStokes.SmoothFourierData.xJet (p : ℕ) (f : TorusInverse.Plane → ℂ) :

TorusInverse.Plane → ℂ

X jet, given by partialX^[p] f.

Equations

NavierStokes.SmoothFourierData.xJet p f = NavierStokes.SmoothFourierData.partialX ^[p] f

Instances For

@[simp]

theorem NavierStokes.SmoothFourierData.xJet_zero (f : TorusInverse.Plane → ℂ) :

xJet 0 f = f

theorem NavierStokes.SmoothFourierData.xJet_succ (p : ℕ) (f : TorusInverse.Plane → ℂ) :

xJet (p + 1) f = partialX (xJet p f)

theorem NavierStokes.SmoothFourierData.partialX_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) :

ContDiff ℝ (↑⊤) (partialX f)

theorem NavierStokes.SmoothFourierData.xJet_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (p : ℕ) :

ContDiff ℝ (↑⊤) (xJet p f)

theorem NavierStokes.SmoothFourierData.partialX_periodic {f : TorusInverse.Plane → ℂ} (hf : UnitPeriodic f) :

UnitPeriodic (partialX f)

theorem NavierStokes.SmoothFourierData.xJet_periodic {f : TorusInverse.Plane → ℂ} (hf : UnitPeriodic f) (p : ℕ) :

UnitPeriodic (xJet p f)

theorem NavierStokes.SmoothFourierData.hasDerivAt_slice {f : TorusInverse.Plane → ℂ} {x y : ℝ} (hf : DifferentiableAt ℝ f (x, y)) :

HasDerivAt (fun (t : ℝ) => f (t, y)) (partialX f (x, y)) x

noncomputable def NavierStokes.SmoothFourierData.coefficient (f : TorusInverse.Plane → ℂ) (k : TorusInverse.Frequency) :

The actual two-dimensional Fourier coefficient, with the first coordinate integrated first.

Equations

NavierStokes.SmoothFourierData.coefficient f k = NavierStokes.SmoothFourierData.unitCoeff (fun (y : ℝ) => NavierStokes.SmoothFourierData.unitCoeff (fun (x : ℝ) => f (x, y)) k.1) k.2

Instances For

theorem NavierStokes.SmoothFourierData.coefficient_norm_le {f : TorusInverse.Plane → ℂ} {C : ℝ} (k : TorusInverse.Frequency) (hb : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖f (x, y)‖ ≤ C) :

‖coefficient f k‖ ≤ C

theorem NavierStokes.SmoothFourierData.coefficient_partialX {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) {k : TorusInverse.Frequency} (hk : k.1 ≠ 0) :

coefficient f k = (TorusInverse.omega * ↑k.1)⁻¹ * coefficient (partialX f) k

theorem NavierStokes.SmoothFourierData.coefficient_xJet {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) {k : TorusInverse.Frequency} (hk : k.1 ≠ 0) (p : ℕ) :

coefficient f k = (TorusInverse.omega * ↑k.1)⁻¹ ^ p * coefficient (xJet p f) k

Repeated Fourier integration by parts in the first coordinate.

theorem NavierStokes.SmoothFourierData.coefficient_decay_first {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) {k : TorusInverse.Frequency} (hk : k.1 ≠ 0) (p : ℕ) {C : ℝ} (hb : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet p f (x, y)‖ ≤ C) :

‖coefficient f k‖ ≤ ‖(TorusInverse.omega * ↑k.1)⁻¹ ‖ ^ p * C

A coefficient-decay estimate obtained from a bound on an actual derivative.

noncomputable def NavierStokes.SmoothFourierData.kernel (k : TorusInverse.Frequency) (z : TorusInverse.Plane) :

The negative Fourier character on the unit square.

Equations

NavierStokes.SmoothFourierData.kernel k z = (fourier (-k.1)) ↑z.1 * (fourier (-k.2)) ↑z.2

Instances For

theorem NavierStokes.SmoothFourierData.kernel_continuous (k : TorusInverse.Frequency) :

Continuous (kernel k)

theorem NavierStokes.SmoothFourierData.coefficient_eq_doubleIntegral (f : TorusInverse.Plane → ℂ) (k : TorusInverse.Frequency) :

coefficient f k = ∫ (y : ℝ) (x : ℝ) in 0..1, kernel k (x, y) * f (x, y)

theorem NavierStokes.SmoothFourierData.integral_square_swap {f : TorusInverse.Plane → ℂ} (hf : Continuous f) :

∫ (y : ℝ) (x : ℝ) in 0..1, f (x, y) = ∫ (x : ℝ) (y : ℝ) in 0..1, f (x, y)

noncomputable def NavierStokes.SmoothFourierData.swapFunction (f : TorusInverse.Plane → ℂ) :

TorusInverse.Plane → ℂ

Swap function, defined pointwise by f (z.2, z.1).

Equations

NavierStokes.SmoothFourierData.swapFunction f z = f (z.2, z.1)

Instances For

theorem NavierStokes.SmoothFourierData.swapFunction_smooth {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) :

ContDiff ℝ (↑⊤) (swapFunction f)

theorem NavierStokes.SmoothFourierData.swapFunction_periodic {f : TorusInverse.Plane → ℂ} (hp : UnitPeriodic f) :

UnitPeriodic (swapFunction f)

theorem NavierStokes.SmoothFourierData.coefficient_swap {f : TorusInverse.Plane → ℂ} (hf : Continuous f) (k : TorusInverse.Frequency) :

coefficient f k = coefficient (swapFunction f) (k.2, k.1)

theorem NavierStokes.SmoothFourierData.coefficient_decay_second {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) {k : TorusInverse.Frequency} (hk : k.2 ≠ 0) (p : ℕ) {C : ℝ} (hb : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet p (swapFunction f) (x, y)‖ ≤ C) :

‖coefficient f k‖ ≤ ‖(TorusInverse.omega * ↑k.2)⁻¹ ‖ ^ p * C

theorem NavierStokes.SmoothFourierData.norm_omega_ge_one :

1 ≤ ‖TorusInverse.omega ‖

theorem NavierStokes.SmoothFourierData.coefficient_first_moment {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) {k : TorusInverse.Frequency} (hk : k.1 ≠ 0) (p : ℕ) {C : ℝ} (hb : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet p f (x, y)‖ ≤ C) :

|↑k.1| ^ p * ‖coefficient f k‖ ≤ C

Multiplying by the first frequency power is controlled by the actual derivative norm.

theorem NavierStokes.SmoothFourierData.dominant_coordinate_ne_zero {k : TorusInverse.Frequency} (hk : k ≠ 0) (hdom : |↑k.2| ≤ |↑k.1|) :

k.1 ≠ 0

theorem NavierStokes.SmoothFourierData.weight_le_dominant {k : TorusInverse.Frequency} (hk : k.1 ≠ 0) (hdom : |↑k.2| ≤ |↑k.1|) :

TorusInverse.weight k ≤ 3 * |↑k.1|

theorem NavierStokes.SmoothFourierData.weight_moment_of_dominant {k : TorusInverse.Frequency} {p : ℕ} {A C : ℝ} (hk : k.1 ≠ 0) (hdom : |↑k.2| ≤ |↑k.1|) (hA : 0 ≤ A) (hb : |↑k.1| ^ p * A ≤ C) :

TorusInverse.weight k ^ p * A ≤ 3 ^ p * C

theorem NavierStokes.SmoothFourierData.coefficient_polynomial_bound {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) (p : ℕ) {C : ℝ} (hzero : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖f (x, y)‖ ≤ C) (hfirst : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet p f (x, y)‖ ≤ C) (hsecond : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet p (swapFunction f) (x, y)‖ ≤ C) (k : TorusInverse.Frequency) :

TorusInverse.weight k ^ p * ‖coefficient f k‖ ≤ 3 ^ p * C

Finite derivative loss: a p-th frequency moment uses only the values and the p-th pure derivative in each coordinate on the unit square.

theorem NavierStokes.SmoothFourierData.exists_coefficient_polynomial_bound {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) (p : ℕ) :

∃ (C : ℝ), ∀ (k : TorusInverse.Frequency), TorusInverse.weight k ^ p * ‖coefficient f k‖ ≤ C

Smoothness on the compact unit square supplies the derivative bounds; no coefficient-decay hypothesis is used.

theorem NavierStokes.SmoothFourierData.summable_integer_weight_inv_two :

Summable fun (n : ℤ) => ((1 + |↑n|) ^ 2)⁻¹

theorem NavierStokes.SmoothFourierData.weight_inv_four_le_product (k : TorusInverse.Frequency) :

(TorusInverse.weight k ^ 4)⁻¹ ≤ ((1 + |↑k.1|) ^ 2)⁻¹ * ((1 + |↑k.2|) ^ 2)⁻¹

theorem NavierStokes.SmoothFourierData.summable_weight_inv_four :

Summable fun (k : TorusInverse.Frequency) => (TorusInverse.weight k ^ 4)⁻¹

theorem NavierStokes.SmoothFourierData.rapid_coefficient {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) :

TorusInverse.Rapid (coefficient f)

Every smooth unit-periodic function has all weighted absolute Fourier moments. For the p-th moment the proof uses p+4 derivatives and a summable lattice majorant.

theorem NavierStokes.SmoothFourierData.coefficient_seminorm_bound {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) (p : ℕ) {C : ℝ} (hzero : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖f (x, y)‖ ≤ C) (hfirst : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet (p + 4) f (x, y)‖ ≤ C) (hsecond : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, ‖xJet (p + 4) (swapFunction f) (x, y)‖ ≤ C) :

TorusInverse.coeffSeminorm p (coefficient f) ≤ 3 ^ (p + 4) * C * ∑' (k : TorusInverse.Frequency), (TorusInverse.weight k ^ 4)⁻¹

A quantitative finite-loss estimate for the exact seminorm used by TorusInverse. The lattice constant is finite by summable_weight_inv_four.

Identification with the actual torus Fourier coefficients #

noncomputable def NavierStokes.SmoothFourierData.torusLift (f : TorusInverse.Torus → ℂ) (x : TorusInverse.Plane) :

Torus lift, given by f ((x.1 : UnitAddCircle), (x.2 : UnitAddCircle)).

Equations

NavierStokes.SmoothFourierData.torusLift f x = f (↑x.1, ↑x.2)

Instances For

theorem NavierStokes.SmoothFourierData.torusLift_periodic (f : TorusInverse.Torus → ℂ) :

UnitPeriodic (torusLift f)

noncomputable def NavierStokes.SmoothFourierData.torusCoefficient (f : TorusInverse.Torus → ℂ) (k : TorusInverse.Frequency) :

Torus coefficient, given by ∫ z, torusMode (-k) z * f z ∂torusMeasure.

Equations

NavierStokes.SmoothFourierData.torusCoefficient f k = ∫ (z : NavierStokes.TorusInverse.Torus), (NavierStokes.TorusInverse.torusMode (-k)) z * f z ∂NavierStokes.TorusInverse.torusMeasure

Instances For

theorem NavierStokes.SmoothFourierData.unitCoeff_torusLift (f : UnitAddCircle → ℂ) (n : ℤ) :

unitCoeff (fun (x : ℝ) => f ↑x) n = fourierCoeff f n

theorem NavierStokes.SmoothFourierData.torusCoefficient_integrable (f : C(TorusInverse.Torus , ℂ )) (k : TorusInverse.Frequency) :

MeasureTheory.Integrable (fun (z : TorusInverse.Torus) => (TorusInverse.torusMode (-k)) z * f z) TorusInverse.torusMeasure

theorem NavierStokes.SmoothFourierData.coefficient_lift_eq_torus (f : C(TorusInverse.Torus , ℂ )) (k : TorusInverse.Frequency) :

coefficient (torusLift ⇑f) k = torusCoefficient (⇑f) k

noncomputable def NavierStokes.SmoothFourierData.nativeFunction (f : C(TorusInverse.Torus , ℂ )) :

C(UnitAddTorus (Fin 2), ℂ )

The same continuous function on Mathlib's native finite-product torus.

Equations

NavierStokes.SmoothFourierData.nativeFunction f = { toFun := fun (z : UnitAddTorus (Fin 2)) => f (z 0, z 1), continuous_toFun := ⋯ }

Instances For

theorem NavierStokes.SmoothFourierData.native_mode_eq (k : Fin 2 → ℤ) (z : UnitAddTorus (Fin 2)) :

(UnitAddTorus.mFourier k) z = (TorusInverse.torusMode (k 0, k 1)) (z 0, z 1)

theorem NavierStokes.SmoothFourierData.native_coefficient_eq (f : C(TorusInverse.Torus , ℂ )) (k : Fin 2 → ℤ) :

UnitAddTorus.mFourierCoeff (⇑(nativeFunction f)) k = torusCoefficient ⇑f (k 0, k 1)

theorem NavierStokes.SmoothFourierData.torusSeries_coefficient (f : C(TorusInverse.Torus , ℂ )) (hf : ContDiff ℝ (↑⊤) (torusLift ⇑f)) (z : TorusInverse.Torus) :

TorusInverse.torusSeries (coefficient (torusLift ⇑f)) z = f z

Genuine Fourier reconstruction: summability is derived from smoothness.

theorem NavierStokes.SmoothFourierData.series_coefficient_lift (f : C(TorusInverse.Torus , ℂ )) (hf : ContDiff ℝ (↑⊤) (torusLift ⇑f)) (x : TorusInverse.Plane) :

TorusInverse.series (coefficient (torusLift ⇑f)) x = torusLift (⇑f) x

theorem NavierStokes.SmoothFourierData.coefficient_zero_eq_mean (f : C(TorusInverse.Torus , ℂ )) :

coefficient (torusLift ⇑f) 0 = ∫ (z : TorusInverse.Torus), f z ∂TorusInverse.torusMeasure

theorem NavierStokes.SmoothFourierData.inverse_solves_smooth_torus (d : TorusInverse.Direction) (f : C(TorusInverse.Torus , ℂ )) (hf : ContDiff ℝ (↑⊤) (torusLift ⇑f)) (hmean : ∫ (z : TorusInverse.Torus), f z ∂TorusInverse.torusMeasure = 0) (x : TorusInverse.Plane) :

(fderiv ℝ (TorusInverse.directionalInverse d (coefficient (torusLift ⇑f))) x) (TorusInverse.vector d) = torusLift (⇑f) x

The constructed inverse now solves the equation for an arbitrary smooth zero-mean torus function, not only for a preassigned coefficient sequence.

Descent of an arbitrary periodic function on the plane #

theorem NavierStokes.SmoothFourierData.unitPeriodic_first {f : TorusInverse.Plane → ℂ} (hp : UnitPeriodic f) (y : ℝ) :

Function.Periodic (fun (x : ℝ) => f (x, y)) 1

theorem NavierStokes.SmoothFourierData.unitPeriodic_second {f : TorusInverse.Plane → ℂ} (hp : UnitPeriodic f) (x : ℝ) :

Function.Periodic (fun (y : ℝ) => f (x, y)) 1

noncomputable def NavierStokes.SmoothFourierData.firstLift (f : TorusInverse.Plane → ℂ) (hp : UnitPeriodic f) (z : UnitAddCircle) (y : ℝ) :

First lift, given by (unitPeriodic_first hp y).lift z.

Equations

NavierStokes.SmoothFourierData.firstLift f hp z y = ⋯.lift z

Instances For

theorem NavierStokes.SmoothFourierData.firstLift_periodic (f : TorusInverse.Plane → ℂ) (hp : UnitPeriodic f) (z : UnitAddCircle) :

Function.Periodic (firstLift f hp z) 1

noncomputable def NavierStokes.SmoothFourierData.descend (f : TorusInverse.Plane → ℂ) (hp : UnitPeriodic f) (z : TorusInverse.Torus) :

Descend, given by (firstLift_periodic f hp z.1).lift z.2.

Equations

NavierStokes.SmoothFourierData.descend f hp z = ⋯.lift z.2

Instances For

@[simp]

theorem NavierStokes.SmoothFourierData.descend_coe (f : TorusInverse.Plane → ℂ) (hp : UnitPeriodic f) (x y : ℝ) :

descend f hp (↑x, ↑y) = f (x, y)

theorem NavierStokes.SmoothFourierData.descend_continuous {f : TorusInverse.Plane → ℂ} (hf : Continuous f) (hp : UnitPeriodic f) :

Continuous (descend f hp)

noncomputable def NavierStokes.SmoothFourierData.descendContinuous (f : TorusInverse.Plane → ℂ) (hf : Continuous f) (hp : UnitPeriodic f) :

C(TorusInverse.Torus , ℂ )

Descend continuous, bundling toFun, continuous_toFun.

Equations

NavierStokes.SmoothFourierData.descendContinuous f hf hp = { toFun := NavierStokes.SmoothFourierData.descend f hp, continuous_toFun := ⋯ }

Instances For

@[simp]

theorem NavierStokes.SmoothFourierData.torusLift_descendContinuous (f : TorusInverse.Plane → ℂ) (hf : Continuous f) (hp : UnitPeriodic f) :

torusLift ⇑(descendContinuous f hf hp) = f

theorem NavierStokes.SmoothFourierData.series_coefficient {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) (x : TorusInverse.Plane) :

TorusInverse.series (coefficient f) x = f x

Pointwise reconstruction for an arbitrary actual smooth unit-periodic function on the plane; neither rapid decay nor reconstruction is a premise.

theorem NavierStokes.SmoothFourierData.coefficient_zero_eq_integral (f : TorusInverse.Plane → ℂ) :

coefficient f 0 = ∫ (y : ℝ) (x : ℝ) in 0..1, f (x, y)

theorem NavierStokes.SmoothFourierData.smooth_periodic_fourier_data {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) :

TorusInverse.Rapid (coefficient f) ∧ TorusInverse.series (coefficient f) = f

The final coefficient bridge to the existing inverse construction.

theorem NavierStokes.SmoothFourierData.inverse_solves_smooth_periodic (d : TorusInverse.Direction) {f : TorusInverse.Plane → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hp : UnitPeriodic f) (hmean : ∫ (y : ℝ) (x : ℝ) in 0..1, f (x, y) = 0) (x : TorusInverse.Plane) :

(fderiv ℝ (TorusInverse.directionalInverse d (coefficient f)) x) (TorusInverse.vector d) = f x