Finite integer-harmonic fields

The coefficients form a genuine finite group algebra. Evaluation is the literal exponential sum, multiplication is convolution, and angular means are actual interval integrals over a period of length 2*pi.

@[reducible, inline]

abbrev NavierStokes.HarmonicFields.Coefficients (α : Type u_1) : Type u_1

Coefficients: an abbreviation for AddMonoidAlgebra (α → ℂ) ℤ.

Equations

• NavierStokes.HarmonicFields.Coefficients α = AddMonoidAlgebra (α → ℂ) ℤ

@[instance_reducible]

instance NavierStokes.HarmonicFields.instCoeFunCoefficientsForallIntForallComplex {α : Type u_1} : CoeFun (Coefficients α) fun (x : Coefficients α) => ℤ → α → ℂ

Coefficient access for the wrapped group algebra.

Equations

• NavierStokes.HarmonicFields.instCoeFunCoefficientsForallIntForallComplex = { coe := fun (c : NavierStokes.HarmonicFields.Coefficients α) => ⇑c.coeff }

@[reducible, inline]

abbrev NavierStokes.HarmonicFields.Coefficients.support {α : Type u_1} (c : Coefficients α) : Finset ℤ

Support: an abbreviation for c.coeff.support.

Equations

• c.support = c.coeff.support

@[reducible, inline]

abbrev NavierStokes.HarmonicFields.Coefficients.sum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : Coefficients α) (f : ℤ → (α → ℂ) → M) : M

Sum: an abbreviation for c.coeff.sum f.

Equations

• c.sum f = c.coeff.sum f

noncomputable def NavierStokes.HarmonicFields.character (j : ℤ) (φ : ℝ) : ℂ

Character, given by Complex.exp ((j : ℂ) * (φ : ℂ) * Complex.I).

Equations

• NavierStokes.HarmonicFields.character j φ = Complex.exp (↑j * ↑φ * Complex.I)

@[simp]

theorem NavierStokes.HarmonicFields.character_zero (φ : ℝ) : character 0 φ = 1

theorem NavierStokes.HarmonicFields.character_add (i j : ℤ) (φ : ℝ) : character (i + j) φ = character i φ * character j φ

theorem NavierStokes.HarmonicFields.character_phase_add (j : ℤ) (φ ψ : ℝ) : character j (φ + ψ) = character j φ * character j ψ

theorem NavierStokes.HarmonicFields.character_int_mul (j kp : ℤ) (θ : ℝ) : character j (↑kp * θ) = character (j * kp) θ

@[simp]

theorem NavierStokes.HarmonicFields.norm_character (j : ℤ) (φ : ℝ) : ‖character j φ‖ = 1

theorem NavierStokes.HarmonicFields.character_neg (j : ℤ) (φ : ℝ) : character (-j) φ = (starRingEnd ℂ) (character j φ)

theorem NavierStokes.HarmonicFields.character_continuous (j : ℤ) : Continuous (character j)

noncomputable def NavierStokes.HarmonicFields.characterHom (φ : ℝ) : Multiplicative ℤ →* ℂ

Character hom, bundling toFun, map_one, map_mul.

Equations

• NavierStokes.HarmonicFields.characterHom φ = { toFun := fun (j : Multiplicative ℤ) => NavierStokes.HarmonicFields.character (Multiplicative.toAdd j) φ, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def NavierStokes.HarmonicFields.evaluateHom {α : Type u_1} (x : α) (φ : ℝ) : Coefficients α →+* ℂ

Evaluate hom, given by AddMonoidAlgebra.liftNCRingHom (Pi.evalRingHom (fun _ : α => ℂ) x) (characterHom φ) (fun _ _ => Commute.all _ _).

Equations

• NavierStokes.HarmonicFields.evaluateHom x φ = AddMonoidAlgebra.liftNCRingHom (Pi.evalRingHom (fun (x : α) => ℂ) x) (NavierStokes.HarmonicFields.characterHom φ) ⋯

noncomputable def NavierStokes.HarmonicFields.evaluate {α : Type u_1} (c : Coefficients α) (x : α) (φ : ℝ) : ℂ

Evaluate, given by c.sum (fun j a => a x * character j φ).

Equations

• NavierStokes.HarmonicFields.evaluate c x φ = c.sum fun (j : ℤ) (a : α → ℂ) => a x * NavierStokes.HarmonicFields.character j φ

theorem NavierStokes.HarmonicFields.evaluate_eq_hom {α : Type u_1} (c : Coefficients α) (x : α) (φ : ℝ) : evaluate c x φ = (evaluateHom x φ) c

@[simp]

theorem NavierStokes.HarmonicFields.evaluate_zero {α : Type u_1} (x : α) (φ : ℝ) : evaluate 0 x φ = 0

theorem NavierStokes.HarmonicFields.evaluate_add {α : Type u_1} (c d : Coefficients α) (x : α) (φ : ℝ) : evaluate (c + d) x φ = evaluate c x φ + evaluate d x φ

theorem NavierStokes.HarmonicFields.evaluate_mul {α : Type u_1} (c d : Coefficients α) (x : α) (φ : ℝ) : evaluate (c * d) x φ = evaluate c x φ * evaluate d x φ

The actual product of two finite fields is evaluation of the finite coefficient convolution.

theorem NavierStokes.HarmonicFields.evaluate_single {α : Type u_1} (j : ℤ) (a : α → ℂ) (x : α) (φ : ℝ) : evaluate (AddMonoidAlgebra.single j a) x φ = a x * character j φ

theorem NavierStokes.HarmonicFields.evaluate_over {α : Type u_1} (c : Coefficients α) (s : Finset ℤ) (hs : c.support ⊆ s) (x : α) (φ : ℝ) : evaluate c x φ = ∑ j ∈ s, c.coeff j x * character j φ

noncomputable def NavierStokes.HarmonicFields.field {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : ℂ

The slow/auxiliary parameter is x. Its coefficient functions have no angular input. The angular frequency is the literal integer j*kp.

Equations

• NavierStokes.HarmonicFields.field c k Φ kp p = NavierStokes.HarmonicFields.evaluate c p.1 (k * Φ p.1 + ↑kp * p.2)

theorem NavierStokes.HarmonicFields.field_expansion {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (x : α) (θ : ℝ) : field c k Φ kp (x, θ) = ∑ j ∈ c.support, c.coeff j x * character j (k * Φ x) * character (j * kp) θ

theorem NavierStokes.HarmonicFields.field_mul {α : Type u_1} (c d : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : field (c * d) k Φ kp p = field c k Φ kp p * field d k Φ kp p

theorem NavierStokes.HarmonicFields.field_angular_continuous {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (x : α) : Continuous fun (θ : ℝ) => field c k Φ kp (x, θ)

noncomputable def NavierStokes.HarmonicFields.period : ℝ

Period, given by 2 * Real.pi.

Equations

• NavierStokes.HarmonicFields.period = 2 * Real.pi

theorem NavierStokes.HarmonicFields.period_pos : 0 < period

theorem NavierStokes.HarmonicFields.period_ne_zero : period ≠ 0

noncomputable def NavierStokes.HarmonicFields.angularMean (f : ℝ → ℂ) : ℂ

This is a genuine normalized angular integral.

Equations

• NavierStokes.HarmonicFields.angularMean f = (↑NavierStokes.HarmonicFields.period)⁻¹ * ∫ (θ : ℝ) in 0..NavierStokes.HarmonicFields.period, f θ

theorem NavierStokes.HarmonicFields.character_period (j : ℤ) : character j period = 1

theorem NavierStokes.HarmonicFields.character_periodic (j : ℤ) : Function.Periodic (character j) period

theorem NavierStokes.HarmonicFields.field_angular_periodic {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (x : α) : Function.Periodic (fun (θ : ℝ) => field c k Φ kp (x, θ)) period

theorem NavierStokes.HarmonicFields.integral_character (j : ℤ) : ∫ (θ : ℝ) in 0..period, character j θ = if j = 0 then ↑period else 0

theorem NavierStokes.HarmonicFields.angularMean_const_character (A : ℂ) (j : ℤ) : (angularMean fun (θ : ℝ) => A * character j θ) = if j = 0 then A else 0

theorem NavierStokes.HarmonicFields.angularMean_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℝ → ℂ) (hf : ∀ i ∈ s, Continuous (f i)) : (angularMean fun (θ : ℝ) => ∑ i ∈ s, f i θ) = ∑ i ∈ s, angularMean (f i)

theorem NavierStokes.HarmonicFields.angularMean_field {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : α) : (angularMean fun (θ : ℝ) => field c k Φ kp (x, θ)) = c.coeff 0 x

Nonzero integer angular frequency makes the actual angular mean pick precisely the zero harmonic, regardless of the slow phase or carrier band.

noncomputable def NavierStokes.HarmonicFields.coefficientMass {α : Type u_1} (c : Coefficients α) (x : α) : ℝ

Coefficient mass, given by ∑ j ∈ c.support, ‖c j x‖.

Equations

• NavierStokes.HarmonicFields.coefficientMass c x = ∑ j ∈ c.support, ‖c.coeff j x‖

theorem NavierStokes.HarmonicFields.coefficientMass_nonneg {α : Type u_1} (c : Coefficients α) (x : α) : 0 ≤ coefficientMass c x

theorem NavierStokes.HarmonicFields.norm_evaluate_le_mass {α : Type u_1} (c : Coefficients α) (x : α) (φ : ℝ) : ‖evaluate c x φ‖ ≤ coefficientMass c x

A value estimate with constant one, independent of every frequency and of the largest occupied harmonic.

theorem NavierStokes.HarmonicFields.norm_field_le_mass {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : ‖field c k Φ kp p‖ ≤ coefficientMass c p.1

theorem NavierStokes.HarmonicFields.norm_field_product_le {α : Type u_1} (c d : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : ‖field (c * d) k Φ kp p‖ ≤ coefficientMass c p.1 * coefficientMass d p.1

theorem NavierStokes.HarmonicFields.convolution_apply {α : Type u_1} (c d : Coefficients α) (m : ℤ) (x : α) : (c * d).coeff m x = ∑ j ∈ c.support, c.coeff j x * d.coeff (m - j) x

theorem NavierStokes.HarmonicFields.angularMean_product {α : Type u_1} (c d : Coefficients α) (k : ℝ) (Φ : α → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : α) : (angularMean fun (θ : ℝ) => field c k Φ kp (x, θ) * field d k Φ kp (x, θ)) = ∑ j ∈ c.support, c.coeff j x * d.coeff (-j) x

noncomputable def NavierStokes.HarmonicFields.conjugateReverse {α : Type u_1} (c : Coefficients α) : Coefficients α

Conjugate reverse, constructed using AddMonoidAlgebra.ofCoeff.

Equations

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

@[simp]

theorem NavierStokes.HarmonicFields.conjugateReverse_apply {α : Type u_1} (c : Coefficients α) (j : ℤ) (x : α) : (conjugateReverse c).coeff j x = (starRingEnd ℂ) (c.coeff (-j) x)

theorem NavierStokes.HarmonicFields.evaluate_conjugateReverse {α : Type u_1} (c : Coefficients α) (x : α) (φ : ℝ) : evaluate (conjugateReverse c) x φ = (starRingEnd ℂ) (evaluate c x φ)

def NavierStokes.HarmonicFields.ConjugateSymmetric {α : Type u_1} (c : Coefficients α) : Prop

Conjugate symmetric, given by ∀ j x, c (-j) x = conj (c j x).

Equations

• NavierStokes.HarmonicFields.ConjugateSymmetric c = ∀ (j : ℤ) (x : α), c.coeff (-j) x = (starRingEnd ℂ) (c.coeff j x)

theorem NavierStokes.HarmonicFields.conjugateReverse_eq_self {α : Type u_1} {c : Coefficients α} (hc : ConjugateSymmetric c) : conjugateReverse c = c

theorem NavierStokes.HarmonicFields.evaluate_conj_eq_self {α : Type u_1} {c : Coefficients α} (hc : ConjugateSymmetric c) (x : α) (φ : ℝ) : (starRingEnd ℂ) (evaluate c x φ) = evaluate c x φ

theorem NavierStokes.HarmonicFields.field_real {α : Type u_1} {c : Coefficients α} (hc : ConjugateSymmetric c) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : ↑(field c k Φ kp p).re = field c k Φ kp p

theorem NavierStokes.HarmonicFields.angularMean_coefficient_covariance {α : Type u_1} (c : Coefficients α) {d : Coefficients α} (hd : ConjugateSymmetric d) (k : ℝ) (Φ : α → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (x : α) : (angularMean fun (θ : ℝ) => field c k Φ kp (x, θ) * field d k Φ kp (x, θ)) = ∑ j ∈ c.support, c.coeff j x * (starRingEnd ℂ) (d.coeff j x)

The zero mode of the actual product is the complex coefficient covariance, with conjugacy supplying the negative harmonics.

theorem NavierStokes.HarmonicFields.chart_trace (c : Coefficients ProblemStatement.SpaceTime) (Ψ : ProblemStatement.SpaceTime → ℝ) (kp : ℤ) (hc : ∀ j ∈ c.support, MeanResidual.AngularInvariant (c.coeff j)) (hΨ : ∀ (q : ProblemStatement.SpaceTime) (θ : ℝ), Ψ (MeanResidual.angularShift q θ) = Ψ q + ↑kp * θ) (q : ProblemStatement.SpaceTime) (θ : ℝ) : evaluate c (MeanResidual.angularShift q θ) (Ψ (MeanResidual.angularShift q θ)) = field c 1 Ψ kp (q, θ)

theorem NavierStokes.HarmonicFields.meanResidual_product_covariance (c d : Coefficients ProblemStatement.SpaceTime) (Ψ : ProblemStatement.SpaceTime → ℝ) {kp : ℤ} (hkp : kp ≠ 0) (hc : ∀ j ∈ c.support, MeanResidual.AngularInvariant (c.coeff j)) (hd : ∀ j ∈ d.support, MeanResidual.AngularInvariant (d.coeff j)) (hΨ : ∀ (q : ProblemStatement.SpaceTime) (θ : ℝ), Ψ (MeanResidual.angularShift q θ) = Ψ q + ↑kp * θ) (hconj : ConjugateSymmetric d) (q : ProblemStatement.SpaceTime) : MeanResidual.average (fun (y : ProblemStatement.SpaceTime) => evaluate c y (Ψ y) * evaluate d y (Ψ y)) q = ∑ j ∈ c.support, c.coeff j q * (starRingEnd ℂ) (d.coeff j q)

The coefficient covariance is the actual angular average used by MeanResidual, when coefficients are angularly invariant and the phase has the stated integer angular increment.

def NavierStokes.HarmonicFields.BandLimited {α : Type u_1} (c : Coefficients α) (N : ℕ) : Prop

Band limited, given by ∀ j ∈ c.support, j.natAbs ≤ N.

Equations

• NavierStokes.HarmonicFields.BandLimited c N = ∀ j ∈ c.support, j.natAbs ≤ N

theorem NavierStokes.HarmonicFields.BandLimited.mono {α : Type u_1} {c : Coefficients α} {M N : ℕ} (hc : BandLimited c M) (hMN : M ≤ N) : BandLimited c N

theorem NavierStokes.HarmonicFields.BandLimited.add {α : Type u_1} {c d : Coefficients α} {N : ℕ} (hc : BandLimited c N) (hd : BandLimited d N) : BandLimited (c + d) N

theorem NavierStokes.HarmonicFields.BandLimited.mul {α : Type u_1} {c d : Coefficients α} {M N : ℕ} (hc : BandLimited c M) (hd : BandLimited d N) : BandLimited (c * d) (M + N)

theorem NavierStokes.HarmonicFields.band_single_zero {α : Type u_1} (a : α → ℂ) : BandLimited (AddMonoidAlgebra.single 0 a) 0

noncomputable def NavierStokes.HarmonicFields.constantCoefficient {α : Type u_1} (a : α → ℂ) : Coefficients α

Constant coefficient, given by AddMonoidAlgebra.single 0 a.

Equations

• NavierStokes.HarmonicFields.constantCoefficient a = AddMonoidAlgebra.single 0 a

theorem NavierStokes.HarmonicFields.band_constantCoefficient {α : Type u_1} (a : α → ℂ) : BandLimited (constantCoefficient a) 0

noncomputable def NavierStokes.HarmonicFields.quadraticStep {α : Type u_1} (A B C : α → ℂ) (c : Coefficients α) : Coefficients α

A literal quadratic update with arbitrary slow coefficient functions.

Equations

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

theorem NavierStokes.HarmonicFields.band_quadraticStep {α : Type u_1} (A B C : α → ℂ) {c : Coefficients α} {N : ℕ} (hc : BandLimited c N) : BandLimited (quadraticStep A B C c) (N + N)

noncomputable def NavierStokes.HarmonicFields.quadraticIterate {α : Type u_1} (A B C : ℕ → α → ℂ) (c : Coefficients α) : ℕ → Coefficients α

Quadratic iterate as an element of ℕ → Coefficients α | 0 => c | n + 1 => quadraticStep (A n) (B n) (C n) (quadraticIterate A B C c n).

Equations

• NavierStokes.HarmonicFields.quadraticIterate A B C c 0 = c
• NavierStokes.HarmonicFields.quadraticIterate A B C c n.succ = NavierStokes.HarmonicFields.quadraticStep (A n) (B n) (C n) (NavierStokes.HarmonicFields.quadraticIterate A B C c n)

theorem NavierStokes.HarmonicFields.band_quadraticIterate {α : Type u_1} (A B C : ℕ → α → ℂ) {c : Coefficients α} (hc : BandLimited c 1) (n : ℕ) : BandLimited (quadraticIterate A B C c n) (2 ^ n)

Starting in harmonics {-1,0,1}, the actual convolution update has largest harmonic value at most 2^stage. This is a bound on values, not merely on the number of supported frequencies.

theorem NavierStokes.HarmonicFields.quadratic_angular_frequency_bound {α : Type u_1} (A B C : ℕ → α → ℂ) {c : Coefficients α} (hc : BandLimited c 1) (n : ℕ) (kp : ℤ) {j : ℤ} (hj : j ∈ (quadraticIterate A B C c n).support) : (j * kp).natAbs ≤ 2 ^ n * kp.natAbs

theorem NavierStokes.HarmonicFields.field_quadraticStep {α : Type u_1} (A B C : α → ℂ) (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) : field (quadraticStep A B C c) k Φ kp p = A p.1 + B p.1 * field c k Φ kp p + C p.1 * field c k Φ kp p ^ 2

noncomputable def NavierStokes.HarmonicFields.quadraticEnvelope {α : Type u_1} (A B C : ℕ → α → ℂ) (c : Coefficients α) (x : α) : ℕ → ℝ

Quadratic envelope as an element of ℕ → ℝ | 0 => coefficientMass c x | n + 1 => ‖A n x‖ + ‖B n x‖ * quadraticEnvelope A B C c x n + ‖C n x‖ * quadraticEnvelope A B C c x n ^ 2.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.HarmonicFields.quadraticEnvelope A B C c x 0 = NavierStokes.HarmonicFields.coefficientMass c x

theorem NavierStokes.HarmonicFields.norm_quadraticIterate_le {α : Type u_1} (A B C : ℕ → α → ℂ) (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (p : α × ℝ) (n : ℕ) : ‖field (quadraticIterate A B C c n) k Φ kp p‖ ≤ quadraticEnvelope A B C c p.1 n

The value envelope follows the actual quadratic update and contains no factor involving the harmonic band or its cardinality.

noncomputable def NavierStokes.HarmonicFields.wave {E : Type u_1} (c : Coefficients E) (k : ℝ) (Φ : E → ℝ) (x : E) : ℂ

Wave, given by c.sum (fun j a => HarmonicCalculus.mode (k * (j : ℝ)) Φ a x).

Equations

• NavierStokes.HarmonicFields.wave c k Φ x = c.sum fun (j : ℤ) (a : E → ℂ) => NavierStokes.HarmonicCalculus.mode (k * ↑j) Φ a x

theorem NavierStokes.HarmonicFields.character_eq_carrier {E : Type u_1} (j : ℤ) (k : ℝ) (Φ : E → ℝ) (x : E) : character j (k * Φ x) = HarmonicCalculus.carrier (k * ↑j) Φ x

theorem NavierStokes.HarmonicFields.wave_eq_evaluate {E : Type u_1} (c : Coefficients E) (k : ℝ) (Φ : E → ℝ) (x : E) : wave c k Φ x = evaluate c x (k * Φ x)

noncomputable def NavierStokes.HarmonicFields.derivativeCoefficient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (j : ℤ) (a : E → ℂ) (x : E) : ℂ

Derivative coefficient, given by HarmonicCalculus.along V a x + HarmonicCalculus.phaseFactor (k * (j : ℝ)) * Complex.ofReal (HarmonicCalculus.along V Φ x) * a x.

Equations

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

theorem NavierStokes.HarmonicFields.derivativeCoefficient_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (j : ℤ) : derivativeCoefficient V k Φ j 0 = 0

noncomputable def NavierStokes.HarmonicFields.differentiate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) : Coefficients E

Differentiate, constructed using AddMonoidAlgebra.ofCoeff.

Equations

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

@[simp]

theorem NavierStokes.HarmonicFields.differentiate_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) (j : ℤ) : (differentiate V k Φ c).coeff j = derivativeCoefficient V k Φ j (c.coeff j)

theorem NavierStokes.HarmonicFields.support_differentiate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) : (differentiate V k Φ c).support ⊆ c.support

theorem NavierStokes.HarmonicFields.BandLimited.differentiate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) {c : Coefficients E} {N : ℕ} (hc : BandLimited c N) : BandLimited (HarmonicFields.differentiate V k Φ c) N

theorem NavierStokes.HarmonicFields.wave_differentiate_expansion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) (x : E) : wave (differentiate V k Φ c) k Φ x = ∑ j ∈ c.support, derivativeCoefficient V k Φ j (c.coeff j) x * HarmonicCalculus.carrier (k * ↑j) Φ x

theorem NavierStokes.HarmonicFields.along_wave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) {x : E} (hΦ : DifferentiableAt ℝ Φ x) (hc : ∀ j ∈ c.support, DifferentiableAt ℝ (c.coeff j) x) : HarmonicCalculus.along V (wave c k Φ) x = wave (differentiate V k Φ c) k Φ x

Differentiating the actual finite wave applies the full product rule to each coefficient and phase, and introduces no new harmonic values.

theorem NavierStokes.HarmonicFields.along_field_slow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (kp : ℤ) (c : Coefficients E) (θ : ℝ) {x : E} (hΦ : DifferentiableAt ℝ Φ x) (hc : ∀ j ∈ c.support, DifferentiableAt ℝ (c.coeff j) x) : HarmonicCalculus.along V (fun (y : E) => field c k Φ kp (y, θ)) x = field (differentiate V k Φ c) k Φ kp (x, θ)

theorem NavierStokes.HarmonicFields.derivativeCoefficient_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {V : E → E} {Φ : E → ℝ} {a : E → ℂ} (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (k : ℝ) (j : ℤ) : ContDiffOn ℝ (↑⊤) (derivativeCoefficient V k Φ j a) U

theorem NavierStokes.HarmonicFields.differentiate_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {V : E → E} {Φ : E → ℝ} (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) {c : Coefficients E} (hc : ∀ j ∈ c.support, ContDiffOn ℝ (↑⊤) (c.coeff j) U) (j : ℤ) : j ∈ (differentiate V k Φ c).support → ContDiffOn ℝ (↑⊤) ((differentiate V k Φ c).coeff j) U

noncomputable def NavierStokes.HarmonicFields.iteratedCoefficients {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) (c : Coefficients E) : ℕ → Coefficients E

Iterated coefficients as an element of ℕ → Coefficients E | 0 => c | n + 1 => differentiate V k Φ (iteratedCoefficients V k Φ c n).

Equations

• NavierStokes.HarmonicFields.iteratedCoefficients V k Φ c 0 = c
• NavierStokes.HarmonicFields.iteratedCoefficients V k Φ c n.succ = NavierStokes.HarmonicFields.differentiate V k Φ (NavierStokes.HarmonicFields.iteratedCoefficients V k Φ c n)

noncomputable def NavierStokes.HarmonicFields.iteratedAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) : ℕ → (E → ℂ) → E → ℂ

Iterated along as an element of ℕ → (E → ℂ) → E → ℂ | 0, f => f | n + 1, f => HarmonicCalculus.along V (iteratedAlong V n f).

Equations

• NavierStokes.HarmonicFields.iteratedAlong V 0 x✝ = x✝
• NavierStokes.HarmonicFields.iteratedAlong V n.succ x✝ = NavierStokes.HarmonicCalculus.along V (NavierStokes.HarmonicFields.iteratedAlong V n x✝)

theorem NavierStokes.HarmonicFields.band_iteratedCoefficients {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (k : ℝ) (Φ : E → ℝ) {c : Coefficients E} {N : ℕ} (hc : BandLimited c N) (n : ℕ) : BandLimited (iteratedCoefficients V k Φ c n) N

theorem NavierStokes.HarmonicFields.iteratedCoefficients_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {V : E → E} {Φ : E → ℝ} (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) {c : Coefficients E} (hc : ∀ j ∈ c.support, ContDiffOn ℝ (↑⊤) (c.coeff j) U) (n : ℕ) (j : ℤ) : j ∈ (iteratedCoefficients V k Φ c n).support → ContDiffOn ℝ (↑⊤) ((iteratedCoefficients V k Φ c n).coeff j) U

theorem NavierStokes.HarmonicFields.iteratedAlong_wave {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (hU : IsOpen U) {V : E → E} {Φ : E → ℝ} (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (k : ℝ) {c : Coefficients E} (hc : ∀ j ∈ c.support, ContDiffOn ℝ (↑⊤) (c.coeff j) U) (n : ℕ) : Set.EqOn (iteratedAlong V n (wave c k Φ)) (wave (iteratedCoefficients V k Φ c n) k Φ) U

All repeated actual directional derivatives retain the original finite set of harmonic values. Direction-field derivatives are included.

theorem NavierStokes.HarmonicFields.character_hasDerivAt (j : ℤ) (θ : ℝ) : HasDerivAt (character j) (↑j * Complex.I * character j θ) θ

noncomputable def NavierStokes.HarmonicFields.angularDifferentiate {α : Type u_1} (kp : ℤ) (c : Coefficients α) : Coefficients α

Angular differentiate, constructed using AddMonoidAlgebra.ofCoeff.

Equations

• NavierStokes.HarmonicFields.angularDifferentiate kp c = AddMonoidAlgebra.ofCoeff (Finsupp.onFinset c.support (fun (j : ℤ) (x : α) => ↑(j * kp) * Complex.I * c.coeff j x) ⋯)

@[simp]

theorem NavierStokes.HarmonicFields.angularDifferentiate_apply {α : Type u_1} (kp : ℤ) (c : Coefficients α) (j : ℤ) (x : α) : (angularDifferentiate kp c).coeff j x = ↑(j * kp) * Complex.I * c.coeff j x

theorem NavierStokes.HarmonicFields.support_angularDifferentiate {α : Type u_1} (kp : ℤ) (c : Coefficients α) : (angularDifferentiate kp c).support ⊆ c.support

theorem NavierStokes.HarmonicFields.BandLimited.angularDifferentiate {α : Type u_1} (kp : ℤ) {c : Coefficients α} {N : ℕ} (hc : BandLimited c N) : BandLimited (HarmonicFields.angularDifferentiate kp c) N

theorem NavierStokes.HarmonicFields.field_hasDerivAt_angle {α : Type u_1} (c : Coefficients α) (k : ℝ) (Φ : α → ℝ) (kp : ℤ) (x : α) (θ : ℝ) : HasDerivAt (fun (a : ℝ) => field c k Φ kp (x, a)) (field (angularDifferentiate kp c) k Φ kp (x, θ)) θ

The literal angular derivative acts diagonally on the same harmonic values, with multiplier i*j*kp.