Symmetric extension and parity for the actual Volterra solution

The negative half is obtained by reflecting the differential equation. The integral identity is proved for the glued function at and across the axis; parity will follow from uniqueness, not from the definition of glue.

Regular Volterra inverses and the sparse parameter-derivative system

The radial inverse is an actual interval integral. Its regularity at the axis is proved directly, without interpreting the singular differential expression by division by zero. The analytic word estimates are supplied separately by VolterraAnalyticBounds.

Actual analytic Volterra words for the slow axis recursion

The functions and radial integrals here are genuine functions and Bochner integrals. The parameter derivative is the actual complex derivative.

@[reducible, inline]

abbrev NavierStokes.VolterraAnalyticBounds.Vec : Type

Vector: an abbreviation for Fin 6 → ℂ.

Equations

• NavierStokes.VolterraAnalyticBounds.Vec = (Fin 6 → ℂ)

@[reducible, inline]

abbrev NavierStokes.VolterraAnalyticBounds.Field : Type

Field: an abbreviation for ℝ → ℂ → Vec.

Equations

• NavierStokes.VolterraAnalyticBounds.Field = (ℝ → ℂ → NavierStokes.VolterraAnalyticBounds.Vec)

@[reducible, inline]

abbrev NavierStokes.VolterraAnalyticBounds.Coeff : Type

Coefficient: an abbreviation for ℝ → ℂ → Matrix (Fin 6) (Fin 6) ℂ.

Equations

• NavierStokes.VolterraAnalyticBounds.Coeff = (ℝ → ℂ → Matrix (Fin 6) (Fin 6) ℂ)

noncomputable def NavierStokes.VolterraAnalyticBounds.exponent (i : Fin 6) : ℕ

The singular diagonal in the transformed axis equations is (0, 0, 2, 0, 3, 1), with zero-based component indices.

Equations

• NavierStokes.VolterraAnalyticBounds.exponent i = if ↑i = 2 then 2 else if ↑i = 4 then 3 else if ↑i = 5 then 1 else 0

noncomputable def NavierStokes.VolterraAnalyticBounds.parameterDeriv (F : Field) : Field

Parameter derivative, defined pointwise by deriv (fun w : ℂ => F r w i) z.

Equations

• NavierStokes.VolterraAnalyticBounds.parameterDeriv F r z i = deriv (fun (w : ℂ) => F r w i) z

noncomputable def NavierStokes.VolterraAnalyticBounds.radialInverse (F : Field) : Field

Normalized form of the regular inverse. It includes r = 0 without division by the radial coordinate.

Equations

• NavierStokes.VolterraAnalyticBounds.radialInverse F r z i = r • ∫ (t : ℝ) in 0..1, t ^ NavierStokes.VolterraAnalyticBounds.exponent i • F (t * r) z i

noncomputable def NavierStokes.VolterraAnalyticBounds.matrixAction (A : Coeff) (F : Field) : Field

Matrix action, defined pointwise by (A r z).mulVec (F r z).

Equations

• NavierStokes.VolterraAnalyticBounds.matrixAction A F r z = (A r z).mulVec (F r z)

noncomputable def NavierStokes.VolterraAnalyticBounds.letter (A₀ A₁ : Coeff) (b : Bool) (F : Field) : Field

False is the multiplication letter; true is the parameter-derivative letter.

Equations

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

noncomputable def NavierStokes.VolterraAnalyticBounds.word (A₀ A₁ : Coeff) : List Bool → Field → Field

Word as an element of w, F => letter A₀ A₁ b (word A₀ A₁ w F).

Equations

• NavierStokes.VolterraAnalyticBounds.word A₀ A₁ [] x✝ = x✝
• NavierStokes.VolterraAnalyticBounds.word A₀ A₁ (b :: w) x✝ = NavierStokes.VolterraAnalyticBounds.letter A₀ A₁ b (NavierStokes.VolterraAnalyticBounds.word A₀ A₁ w x✝)

def NavierStokes.VolterraAnalyticBounds.DerivativeShape (A : Coeff) : Prop

Only the last two rows and first four columns may be nonzero.

Equations

• NavierStokes.VolterraAnalyticBounds.DerivativeShape A = ∀ (r : ℝ) (z : ℂ) (i j : Fin 6), ↑i < 4 ∨ 4 ≤ ↑j → A r z i j = 0

def NavierStokes.VolterraAnalyticBounds.LowZero (F : Field) : Prop

Vanishing of the first four components as actual functions.

Equations

• NavierStokes.VolterraAnalyticBounds.LowZero F = ∀ (r : ℝ) (z : ℂ) (i : Fin 6), ↑i < 4 → F r z i = 0

theorem NavierStokes.VolterraAnalyticBounds.lowZero_matrixAction {A : Coeff} (hA : DerivativeShape A) (F : Field) : LowZero (matrixAction A F)

theorem NavierStokes.VolterraAnalyticBounds.lowZero_parameterDeriv {F : Field} (hF : LowZero F) : LowZero (parameterDeriv F)

theorem NavierStokes.VolterraAnalyticBounds.lowZero_radialInverse {F : Field} (hF : LowZero F) : LowZero (radialInverse F)

theorem NavierStokes.VolterraAnalyticBounds.matrixAction_lowZero_eq_zero {A : Coeff} (hA : DerivativeShape A) {F : Field} (hF : LowZero F) : matrixAction A F = 0

@[simp]

theorem NavierStokes.VolterraAnalyticBounds.radialInverse_zero : radialInverse 0 = 0

@[simp]

theorem NavierStokes.VolterraAnalyticBounds.parameterDeriv_zero : parameterDeriv 0 = 0

@[simp]

theorem NavierStokes.VolterraAnalyticBounds.matrixAction_zero (A : Coeff) : matrixAction A 0 = 0

@[simp]

theorem NavierStokes.VolterraAnalyticBounds.letter_zero (A₀ A₁ : Coeff) (b : Bool) : letter A₀ A₁ b 0 = 0

theorem NavierStokes.VolterraAnalyticBounds.derivativeLetter_lowZero (A₀ : Coeff) {A₁ : Coeff} (hA : DerivativeShape A₁) (F : Field) : LowZero (letter A₀ A₁ true F)

theorem NavierStokes.VolterraAnalyticBounds.derivativeLetter_of_lowZero (A₀ : Coeff) {A₁ : Coeff} (hA : DerivativeShape A₁) {F : Field} (hF : LowZero F) : letter A₀ A₁ true F = 0

theorem NavierStokes.VolterraAnalyticBounds.adjacent_derivative_letters_zero (A₀ : Coeff) {A₁ : Coeff} (hA : DerivativeShape A₁) (F : Field) : letter A₀ A₁ true (letter A₀ A₁ true F) = 0

This is an identity of actual differentiated integral operators. The proof differentiates identically zero components, so it includes the terms where the parameter derivative would hit the adjacent coefficient.

noncomputable def NavierStokes.VolterraAnalyticBounds.losses : List Bool → ℕ

The number of parameter-derivative letters.

Equations

• NavierStokes.VolterraAnalyticBounds.losses [] = 0
• NavierStokes.VolterraAnalyticBounds.losses (false :: w) = NavierStokes.VolterraAnalyticBounds.losses w
• NavierStokes.VolterraAnalyticBounds.losses (true :: w) = NavierStokes.VolterraAnalyticBounds.losses w + 1

def NavierStokes.VolterraAnalyticBounds.GoodWord : List Bool → Prop

Words without consecutive parameter-derivative letters.

Equations

• NavierStokes.VolterraAnalyticBounds.GoodWord [] = True
• NavierStokes.VolterraAnalyticBounds.GoodWord (false :: w) = NavierStokes.VolterraAnalyticBounds.GoodWord w
• NavierStokes.VolterraAnalyticBounds.GoodWord [true] = True
• NavierStokes.VolterraAnalyticBounds.GoodWord (true :: false :: w) = NavierStokes.VolterraAnalyticBounds.GoodWord w
• NavierStokes.VolterraAnalyticBounds.GoodWord (true :: true :: tail) = False

theorem NavierStokes.VolterraAnalyticBounds.goodWord_losses (w : List Bool) (hw : GoodWord w) : 2 * losses w ≤ w.length + 1

theorem NavierStokes.VolterraAnalyticBounds.losses_le_half (w : List Bool) (hw : GoodWord w) : losses w ≤ (w.length + 1) / 2

theorem NavierStokes.VolterraAnalyticBounds.word_eq_zero_of_not_good (A₀ : Coeff) {A₁ : Coeff} (hA : DerivativeShape A₁) (w : List Bool) (hw : ¬GoodWord w) (F : Field) : word A₀ A₁ w F = 0

Forbidden words are identically zero, for arbitrary actual input functions.

def NavierStokes.VolterraAnalyticBounds.RadialBound (F : Field) (T : ℝ) (c : ℂ) (ρ B : ℝ) (k : ℕ) : Prop

A factorially normalized radial bound on an actual field.

Equations

• NavierStokes.VolterraAnalyticBounds.RadialBound F T c ρ B k = ∀ r ∈ Set.Icc 0 T, ∀ z ∈ Metric.closedBall c ρ, ∀ (i : Fin 6), ‖F r z i‖ ≤ B * r ^ k / ↑k.factorial

def NavierStokes.VolterraAnalyticBounds.AnalyticField (F : Field) (T : ℝ) (c : ℂ) (ρ : ℝ) : Prop

Coordinatewise holomorphy on a neighborhood of the closed parameter disk.

Equations

• NavierStokes.VolterraAnalyticBounds.AnalyticField F T c ρ = ∀ r ∈ Set.Icc 0 T, ∀ (i : Fin 6), AnalyticOnNhd ℂ (fun (z : ℂ) => F r z i) (Metric.closedBall c ρ)

def NavierStokes.VolterraAnalyticBounds.MatrixBound (A : Coeff) (T : ℝ) (c : ℂ) (ρ M : ℝ) : Prop

A row-sum bound on the actual matrix coefficients.

Equations

• NavierStokes.VolterraAnalyticBounds.MatrixBound A T c ρ M = ∀ r ∈ Set.Icc 0 T, ∀ z ∈ Metric.closedBall c ρ, ∀ (i : Fin 6), ∑ j : Fin 6, ‖A r z i j‖ ≤ M

theorem NavierStokes.VolterraAnalyticBounds.RadialBound.mono_radius {F : Field} {T ρ σ B : ℝ} {c : ℂ} {k : ℕ} (h : RadialBound F T c σ B k) (hρ : ρ ≤ σ) : RadialBound F T c ρ B k

theorem NavierStokes.VolterraAnalyticBounds.MatrixBound.mono_radius {A : Coeff} {T ρ σ M : ℝ} {c : ℂ} (h : MatrixBound A T c σ M) (hρ : ρ ≤ σ) : MatrixBound A T c ρ M

theorem NavierStokes.VolterraAnalyticBounds.RadialBound.matrixAction {A : Coeff} {F : Field} {T ρ B M : ℝ} {c : ℂ} {k : ℕ} (hB : 0 ≤ B) (hA : MatrixBound A T c ρ M) (hF : RadialBound F T c ρ B k) : RadialBound (VolterraAnalyticBounds.matrixAction A F) T c ρ (M * B) k

theorem NavierStokes.VolterraAnalyticBounds.RadialBound.radialInverse {F : Field} {T ρ B : ℝ} {c : ℂ} {k : ℕ} (hB : 0 ≤ B) (hF : RadialBound F T c ρ B k) : RadialBound (VolterraAnalyticBounds.radialInverse F) T c ρ B (k + 1)

The elementary radial integral supplies one full factorial denominator. No radial analyticity, and no estimate on radial derivatives, is used.

theorem NavierStokes.VolterraAnalyticBounds.norm_deriv_le {f : ℂ → ℂ} {c : ℂ} {δ C : ℝ} (hδ : 0 < δ) (hf : DifferentiableOn ℂ f (Metric.closedBall c δ)) (hb : ∀ z ∈ Metric.sphere c δ, ‖f z‖ ≤ C) : ‖deriv f c‖ ≤ C / δ

Cauchy's first derivative estimate from the actual circle integral.

theorem NavierStokes.VolterraAnalyticBounds.nested_closedBall {c z : ℂ} {ρ δ : ℝ} (hz : z ∈ Metric.closedBall c ρ) : Metric.closedBall z δ ⊆ Metric.closedBall c (ρ + δ)

theorem NavierStokes.VolterraAnalyticBounds.RadialBound.parameterDeriv {F : Field} {T ρ δ B : ℝ} {c : ℂ} {k : ℕ} (hδ : 0 < δ) (ha : AnalyticField F T c (ρ + δ)) (hF : RadialBound F T c (ρ + δ) B k) : RadialBound (VolterraAnalyticBounds.parameterDeriv F) T c ρ (B / δ) k

One real Cauchy loss, on a fixed smaller disk, without any radial loss.

theorem NavierStokes.VolterraAnalyticBounds.AnalyticField.mono_radius {F : Field} {T ρ σ : ℝ} {c : ℂ} (h : AnalyticField F T c σ) (hρ : ρ ≤ σ) : AnalyticField F T c ρ

theorem NavierStokes.VolterraAnalyticBounds.RadialBound.mono_const {F : Field} {T ρ B C : ℝ} {c : ℂ} {k : ℕ} (h : RadialBound F T c ρ B k) (hBC : B ≤ C) : RadialBound F T c ρ C k

theorem NavierStokes.VolterraAnalyticBounds.word_radialBound {A₀ A₁ : Coeff} {F : Field} {T σ B M δ : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hδ : 0 < δ) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) (w : List Bool) {ρ : ℝ} (hgap : ρ + ↑(losses w) * δ ≤ σ) : RadialBound (word A₀ A₁ w F) T c ρ (B * M ^ w.length * δ⁻¹ ^ losses w) w.length

The exact word estimate. Holomorphy of the finite words is a regularity input, independently obtained by closure of holomorphic curve-valued maps. Neither a convergent series nor a solution is assumed.

noncomputable def NavierStokes.VolterraAnalyticBounds.halfLength (k : ℕ) : ℕ

Half the word length, rounded upward.

Equations

• NavierStokes.VolterraAnalyticBounds.halfLength k = (k + 1) / 2

noncomputable def NavierStokes.VolterraAnalyticBounds.wordMajorant (a b : ℝ) (k : ℕ) : ℝ

A common majorant for every word of length k, including forbidden words.

Equations

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

theorem NavierStokes.VolterraAnalyticBounds.wordMajorant_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (k : ℕ) : 0 ≤ wordMajorant a b k

theorem NavierStokes.VolterraAnalyticBounds.norm_word_le {A₀ A₁ : Coeff} {F : Field} {T ρ σ B M : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hT : 0 ≤ T) (hgap : ρ < σ) (hshape : DerivativeShape A₁) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) (w : List Bool) {r : ℝ} (hr : r ∈ Set.Icc 0 T) {z : ℂ} (hz : z ∈ Metric.closedBall c ρ) (i : Fin 6) : ‖word A₀ A₁ w F r z i‖ ≤ B * wordMajorant (M * T) (max 1 (σ - ρ)⁻¹) w.length

Uniform bound on an entire finite radial interval. The strip gap is split only among the possible derivative letters, and not among all letters.

theorem NavierStokes.VolterraAnalyticBounds.factorial_half_bound (k : ℕ) : max 1 (halfLength k) ^ halfLength k * (k / 2).factorial ≤ k.factorial

The factorial cancels all powers introduced by at most half as many Cauchy losses, leaving an exponential-series denominator.

theorem NavierStokes.VolterraAnalyticBounds.half_power_div_factorial_le (k : ℕ) : ↑(max 1 (halfLength k)) ^ halfLength k / ↑k.factorial ≤ 1 / ↑(k / 2).factorial

theorem NavierStokes.VolterraAnalyticBounds.wordMajorant_le_exponential {a b : ℝ} (ha : 1 ≤ a) (hb : 1 ≤ b) (k : ℕ) : wordMajorant a b k ≤ a * b * ((a ^ 2 * b) ^ (k / 2) / ↑(k / 2).factorial)

theorem NavierStokes.VolterraAnalyticBounds.wordMajorant_mono {a a' b b' : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (haa : a ≤ a') (hbb : b ≤ b') (k : ℕ) : wordMajorant a b k ≤ wordMajorant a' b' k

theorem NavierStokes.VolterraAnalyticBounds.summable_half_exponential (x C : ℝ) : Summable fun (k : ℕ) => C * (x ^ (k / 2) / ↑(k / 2).factorial)

Repeating each exponential-series term twice preserves summability.

theorem NavierStokes.VolterraAnalyticBounds.summable_wordMajorant {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : Summable (wordMajorant a b)

The Cauchy/Volterra majorant is summable for every finite coefficient, radial, and strip-gap constant. There is no smallness assumption.

theorem NavierStokes.VolterraAnalyticBounds.summable_wordLayers {a b B : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : Summable fun (k : ℕ) => B * 2 ^ k * wordMajorant a b k

The factor 2^k counting all Boolean words is absorbed into the first majorant constant, so the entire Picard layer is still summable.

noncomputable def NavierStokes.VolterraAnalyticBounds.wordLayer (A₀ A₁ : Coeff) (F : Field) (k : ℕ) : Field

The actual finite sum of all words of a fixed length.

Equations

• NavierStokes.VolterraAnalyticBounds.wordLayer A₀ A₁ F k r z i = ∑ v : Fin k → Bool, NavierStokes.VolterraAnalyticBounds.word A₀ A₁ (List.ofFn v) F r z i

theorem NavierStokes.VolterraAnalyticBounds.norm_wordLayer_le {A₀ A₁ : Coeff} {F : Field} {T ρ σ B M : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hT : 0 ≤ T) (hgap : ρ < σ) (hshape : DerivativeShape A₁) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) (k : ℕ) {r : ℝ} (hr : r ∈ Set.Icc 0 T) {z : ℂ} (hz : z ∈ Metric.closedBall c ρ) (i : Fin 6) : ‖wordLayer A₀ A₁ F k r z i‖ ≤ B * 2 ^ k * wordMajorant (M * T) (max 1 (σ - ρ)⁻¹) k

theorem NavierStokes.VolterraAnalyticBounds.summable_norm_wordLayer {A₀ A₁ : Coeff} {F : Field} {T ρ σ B M : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hT : 0 ≤ T) (hgap : ρ < σ) (hshape : DerivativeShape A₁) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) {r : ℝ} (hr : r ∈ Set.Icc 0 T) {z : ℂ} (hz : z ∈ Metric.closedBall c ρ) (i : Fin 6) : Summable fun (k : ℕ) => ‖wordLayer A₀ A₁ F k r z i‖

Absolute convergence of the actual Volterra-word expansion at every point of a smaller closed parameter disk, uniformly bounded by one summable sequence independent of that point.

theorem NavierStokes.VolterraAnalyticBounds.summable_wordLayer {A₀ A₁ : Coeff} {F : Field} {T ρ σ B M : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hT : 0 ≤ T) (hgap : ρ < σ) (hshape : DerivativeShape A₁) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) {r : ℝ} (hr : r ∈ Set.Icc 0 T) {z : ℂ} (hz : z ∈ Metric.closedBall c ρ) (i : Fin 6) : Summable fun (k : ℕ) => wordLayer A₀ A₁ F k r z i

theorem NavierStokes.VolterraAnalyticBounds.tendstoUniformlyOn_wordLayer {A₀ A₁ : Coeff} {F : Field} {T ρ σ B M : ℝ} {c : ℂ} (hB : 0 ≤ B) (hM : 0 ≤ M) (hT : 0 ≤ T) (hgap : ρ < σ) (hshape : DerivativeShape A₁) (hA₀ : MatrixBound A₀ T c σ M) (hA₁ : MatrixBound A₁ T c σ M) (hF : RadialBound F T c σ B 0) (ha : ∀ (v : List Bool), AnalyticField (word A₀ A₁ v F) T c σ) (i : Fin 6) : TendstoUniformlyOn (fun (N : ℕ) (p : ℝ × ℂ) => ∑ k ∈ Finset.range N, wordLayer A₀ A₁ F k p.1 p.2 i) (fun (p : ℝ × ℂ) => ∑' (k : ℕ), wordLayer A₀ A₁ F k p.1 p.2 i) Filter.atTop (Set.Icc 0 T ×ˢ Metric.closedBall c ρ)

Uniform convergence of the actual partial sums on every smaller closed parameter disk and the entire fixed radial interval.

noncomputable def NavierStokes.NilpotentVolterra.weightedMean {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) (ξ : ℝ) : E

The normalized integral in the regular inverse of d/dξ+c/ξ.

Equations

• NavierStokes.NilpotentVolterra.weightedMean c f ξ = ∫ (t : ℝ) in 0..1, t ^ c • f (t * ξ)

noncomputable def NavierStokes.NilpotentVolterra.regularPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) (ξ : ℝ) : E

The genuine zero-axis Volterra inverse.

Equations

• NavierStokes.NilpotentVolterra.regularPrimitive c f ξ = ξ • NavierStokes.NilpotentVolterra.weightedMean c f ξ

theorem NavierStokes.NilpotentVolterra.weightedMean_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) : Continuous (weightedMean c f)

theorem NavierStokes.NilpotentVolterra.regularPrimitive_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) : Continuous (regularPrimitive c f)

@[simp]

theorem NavierStokes.NilpotentVolterra.regularPrimitive_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) : regularPrimitive c f 0 = 0

theorem NavierStokes.NilpotentVolterra.weightedMean_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) (f : ℝ → E) : weightedMean c f 0 = (1 / (↑c + 1)) • f 0

theorem NavierStokes.NilpotentVolterra.regularPrimitive_integratingFactor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) (ξ : ℝ) : ξ ^ c • regularPrimitive c f ξ = ∫ (s : ℝ) in 0..ξ, s ^ c • f s

Multiplication by the integrating factor gives the ordinary primitive.

theorem NavierStokes.NilpotentVolterra.regularPrimitive_eq_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) {ξ : ℝ} (hξ : ξ ≠ 0) : regularPrimitive c f ξ = (ξ ^ c)⁻¹ • ∫ (s : ℝ) in 0..ξ, s ^ c • f s

theorem NavierStokes.NilpotentVolterra.regularPrimitive_hasDerivAt_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) : HasDerivAt (regularPrimitive c f) (weightedMean c f 0) 0

The axis derivative is the normalized average at zero.

theorem NavierStokes.NilpotentVolterra.weightedMean_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) (ξ M : ℝ) (hf : ∀ t ∈ Set.Icc 0 1, ‖f (t * ξ)‖ ≤ M) : ‖weightedMean c f ξ‖ ≤ M

theorem NavierStokes.NilpotentVolterra.regularPrimitive_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℕ) (f : ℝ → E) (ξ M : ℝ) (hf : ∀ t ∈ Set.Icc 0 1, ‖f (t * ξ)‖ ≤ M) : ‖regularPrimitive c f ξ‖ ≤ |ξ| * M

theorem NavierStokes.NilpotentVolterra.regularPrimitive_hasDerivAt_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) {ξ : ℝ} (hξ : ξ ≠ 0) : HasDerivAt (regularPrimitive c f) (f ξ - ↑c • weightedMean c f ξ) ξ

Differentiating the integrating-factor formula gives a nonsingular formula for the radial derivative away from the axis.

theorem NavierStokes.NilpotentVolterra.regularPrimitive_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) (ξ : ℝ) : HasDerivAt (regularPrimitive c f) (f ξ - ↑c • weightedMean c f ξ) ξ

The same derivative formula is valid at zero; no singular division is used to define or differentiate the solution there.

theorem NavierStokes.NilpotentVolterra.regularPrimitive_equation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) {ξ : ℝ} (hξ : ξ ≠ 0) : deriv (regularPrimitive c f) ξ + (↑c / ξ) • regularPrimitive c f ξ = f ξ

theorem NavierStokes.NilpotentVolterra.regularPrimitive_derivative_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (c : ℕ) {f : ℝ → E} (hf : Continuous f) : Continuous (deriv (regularPrimitive c f))

@[reducible, inline]

abbrev NavierStokes.NilpotentVolterra.Vec : Type

The six actual components of the first-order radial system.

Equations

• NavierStokes.NilpotentVolterra.Vec = (Fin 6 → ℂ)

@[reducible, inline]

abbrev NavierStokes.NilpotentVolterra.Path (R : ℝ) : Type

Continuous paths on the full fixed radial interval.

Equations

• NavierStokes.NilpotentVolterra.Path R = C(↑(Set.Icc 0 R), NavierStokes.NilpotentVolterra.Vec)

@[reducible, inline]

abbrev NavierStokes.NilpotentVolterra.CoefficientPath (R : ℝ) : Type

Coefficient path: an abbreviation for C(Icc (0 : ℝ) R, Vec →L[ℂ] Vec).

Equations

• NavierStokes.NilpotentVolterra.CoefficientPath R = C(↑(Set.Icc 0 R), NavierStokes.NilpotentVolterra.Vec →L[ℂ] NavierStokes.NilpotentVolterra.Vec)

noncomputable def NavierStokes.NilpotentVolterra.extendPath {R : ℝ} (hR : 0 ≤ R) (f : Path R) (ξ : ℝ) : Vec

Extend path, given by f (projIcc 0 R hR ξ).

Equations

• NavierStokes.NilpotentVolterra.extendPath hR f ξ = f (Set.projIcc 0 R hR ξ)

theorem NavierStokes.NilpotentVolterra.extendPath_continuous {R : ℝ} (hR : 0 ≤ R) (f : Path R) : Continuous (extendPath hR f)

theorem NavierStokes.NilpotentVolterra.extendPath_apply {R : ℝ} (hR : 0 ≤ R) (f : Path R) (ξ : ↑(Set.Icc 0 R)) : extendPath hR f ↑ξ = f ξ

noncomputable def NavierStokes.NilpotentVolterra.pathInverseValue {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (f : Path R) : Path R

Path inverse value as an element of Path R.

Equations

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

theorem NavierStokes.NilpotentVolterra.norm_pathInverseValue_le {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (f : Path R) : ‖pathInverseValue hR c f‖ ≤ R * ‖f‖

noncomputable def NavierStokes.NilpotentVolterra.pathInverse {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) : Path R →L[ℂ] Path R

The diagonal integral operator is bounded and complex linear on actual paths.

Equations

• NavierStokes.NilpotentVolterra.pathInverse hR c = { toFun := NavierStokes.NilpotentVolterra.pathInverseValue hR c, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous R ⋯

theorem NavierStokes.NilpotentVolterra.pathInverse_apply {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (f : Path R) (ξ : ↑(Set.Icc 0 R)) (i : Fin 6) : ((pathInverse hR c) f) ξ i = ↑ξ • ∫ (t : ℝ) in 0..1, t ^ c i • extendPath hR f (t * ↑ξ) i

noncomputable def NavierStokes.NilpotentVolterra.coefficientActionValue {R : ℝ} (A : CoefficientPath R) (f : Path R) : Path R

Coefficient action value, given by ⟨fun ξ => A ξ (f ξ), A.continuous.clm_apply f.continuous⟩.

Equations

• NavierStokes.NilpotentVolterra.coefficientActionValue A f = { toFun := fun (ξ : ↑(Set.Icc 0 R)) => (A ξ) (f ξ), continuous_toFun := ⋯ }

theorem NavierStokes.NilpotentVolterra.norm_coefficientActionValue_le {R : ℝ} (A : CoefficientPath R) (f : Path R) : ‖coefficientActionValue A f‖ ≤ ‖A‖ * ‖f‖

noncomputable def NavierStokes.NilpotentVolterra.coefficientActionLinear {R : ℝ} : CoefficientPath R →ₗ[ℂ] Path R →ₗ[ℂ] Path R

Coefficient action linear, bundling toFun, toFun, map_add, map_smul and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.NilpotentVolterra.coefficientAction {R : ℝ} : CoefficientPath R →L[ℂ] Path R →L[ℂ] Path R

Pointwise matrix action is a genuine bounded bilinear map of path spaces.

Equations

• NavierStokes.NilpotentVolterra.coefficientAction = NavierStokes.NilpotentVolterra.coefficientActionLinear.mkContinuous₂ 1 ⋯

theorem NavierStokes.NilpotentVolterra.coefficientAction_apply {R : ℝ} (A : CoefficientPath R) (f : Path R) (ξ : ↑(Set.Icc 0 R)) : ((coefficientAction A) f) ξ = (A ξ) (f ξ)

noncomputable def NavierStokes.NilpotentVolterra.pathLetter {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) (b : Bool) (F : ℂ → Path R) : ℂ → Path R

Path letter, defined pointwise by pathInverse hR c (if b then coefficientAction (A₁ z) (deriv F z) else coefficientAction (A₀ z) (F z)).

Equations

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

def NavierStokes.NilpotentVolterra.pathWord {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) : List Bool → (ℂ → Path R) → ℂ → Path R

Path word as an element of w, F => pathLetter hR c A₀ A₁ b (pathWord hR c A₀ A₁ w F).

Equations

• NavierStokes.NilpotentVolterra.pathWord hR c A₀ A₁ [] x✝ = x✝
• NavierStokes.NilpotentVolterra.pathWord hR c A₀ A₁ (b :: w) x✝ = NavierStokes.NilpotentVolterra.pathLetter hR c A₀ A₁ b (NavierStokes.NilpotentVolterra.pathWord hR c A₀ A₁ w x✝)

theorem NavierStokes.NilpotentVolterra.pathLetter_holomorphic {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) (b : Bool) : DifferentiableOn ℂ (pathLetter hR c A₀ A₁ b F) U

theorem NavierStokes.NilpotentVolterra.pathWord_holomorphic {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) (w : List Bool) : DifferentiableOn ℂ (pathWord hR c A₀ A₁ w F) U

Every finite word is holomorphic before any convergence is asserted.

noncomputable def NavierStokes.NilpotentVolterra.pathEvaluation {R : ℝ} (ξ : ↑(Set.Icc 0 R)) (i : Fin 6) : Path R →L[ℂ] ℂ

Path evaluation, given by (ContinuousLinearMap.proj i).comp (ContinuousMap.evalCLM ℂ ξ).

Equations

• NavierStokes.NilpotentVolterra.pathEvaluation ξ i = ContinuousLinearMap.proj i ∘SL ContinuousMap.evalCLM ℂ ξ

theorem NavierStokes.NilpotentVolterra.pathEvaluation_apply {R : ℝ} (ξ : ↑(Set.Icc 0 R)) (i : Fin 6) (f : Path R) : (pathEvaluation ξ i) f = f ξ i

theorem NavierStokes.NilpotentVolterra.pathEvaluation_deriv {R : ℝ} {F : ℂ → Path R} {z : ℂ} (hF : DifferentiableAt ℂ F z) (ξ : ↑(Set.Icc 0 R)) (i : Fin 6) : deriv (fun (w : ℂ) => (F w) ξ i) z = (deriv F z) ξ i

Coordinate evaluation commutes with the genuine complex derivative.

noncomputable def NavierStokes.NilpotentVolterra.rawField {R : ℝ} (hR : 0 ≤ R) (F : ℂ → Path R) : VolterraAnalyticBounds.Field

Raw field, defined pointwise by extendPath hR (F z) r.

Equations

• NavierStokes.NilpotentVolterra.rawField hR F r z = NavierStokes.NilpotentVolterra.extendPath hR (F z) r

noncomputable def NavierStokes.NilpotentVolterra.rawCoefficient {R : ℝ} (hR : 0 ≤ R) (A : ℂ → CoefficientPath R) : VolterraAnalyticBounds.Coeff

Raw coefficient, defined pointwise by LinearMap.toMatrix' (A z (projIcc 0 R hR r)).toLinearMap.

Equations

• NavierStokes.NilpotentVolterra.rawCoefficient hR A r z = LinearMap.toMatrix' ↑((A z) (Set.projIcc 0 R hR r))

theorem NavierStokes.NilpotentVolterra.rawCoefficient_mulVec {R : ℝ} (hR : 0 ≤ R) (A : ℂ → CoefficientPath R) (r : ℝ) (z : ℂ) (v : Vec) : (rawCoefficient hR A r z).mulVec v = ((A z) (Set.projIcc 0 R hR r)) v

theorem NavierStokes.NilpotentVolterra.rawField_deriv {R : ℝ} (hR : 0 ≤ R) {F : ℂ → Path R} {z : ℂ} (hF : DifferentiableAt ℂ F z) (r : ℝ) : VolterraAnalyticBounds.parameterDeriv (rawField hR F) r z = rawField hR (deriv F) r z

theorem NavierStokes.NilpotentVolterra.scaled_radius_mem {R r t : ℝ} (hr : r ∈ Set.Icc 0 R) (ht : t ∈ Set.Icc 0 1) : t * r ∈ Set.Icc 0 R

theorem NavierStokes.NilpotentVolterra.rawField_pathLetter {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) {F : ℂ → Path R} {z : ℂ} (hF : DifferentiableAt ℂ F z) (b : Bool) {r : ℝ} (hr : r ∈ Set.Icc 0 R) : rawField hR (pathLetter hR VolterraAnalyticBounds.exponent A₀ A₁ b F) r z = VolterraAnalyticBounds.letter (rawCoefficient hR A₀) (rawCoefficient hR A₁) b (rawField hR F) r z

Every path letter is the actual integral/derivative letter on its radial interval.

theorem NavierStokes.NilpotentVolterra.letter_congrOn {R : ℝ} {U : Set ℂ} (hU : IsOpen U) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (b : Bool) {F G : VolterraAnalyticBounds.Field} (hFG : ∀ r ∈ Set.Icc 0 R, ∀ z ∈ U, F r z = G r z) {r : ℝ} (hr : r ∈ Set.Icc 0 R) {z : ℂ} (hz : z ∈ U) : VolterraAnalyticBounds.letter A₀ A₁ b F r z = VolterraAnalyticBounds.letter A₀ A₁ b G r z

theorem NavierStokes.NilpotentVolterra.rawField_pathWord {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) (w : List Bool) {r : ℝ} (hr : r ∈ Set.Icc 0 R) {z : ℂ} (hz : z ∈ U) : VolterraAnalyticBounds.word (rawCoefficient hR A₀) (rawCoefficient hR A₁) w (rawField hR F) r z = rawField hR (pathWord hR VolterraAnalyticBounds.exponent A₀ A₁ w F) r z

The finite path construction represents precisely the raw Volterra words.

theorem NavierStokes.NilpotentVolterra.raw_word_analytic {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ : ℝ} (hDisk : Metric.closedBall center ρ ⊆ U) (w : List Bool) : VolterraAnalyticBounds.AnalyticField (VolterraAnalyticBounds.word (rawCoefficient hR A₀) (rawCoefficient hR A₁) w (rawField hR F)) R center ρ

def NavierStokes.NilpotentVolterra.binaryWords : ℕ → List (List Bool)

Binary words as an element of ℕ → List (List Bool) | 0 => [[]] | k + 1 => (binaryWords k).map (List.cons false) ++ (binaryWords k).map (List.cons true).

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.NilpotentVolterra.binaryWords 0 = [[]]

theorem NavierStokes.NilpotentVolterra.binaryWords_length (k : ℕ) : (binaryWords k).length = 2 ^ k

theorem NavierStokes.NilpotentVolterra.length_of_mem_binaryWords {k : ℕ} {w : List Bool} (hw : w ∈ binaryWords k) : w.length = k

theorem NavierStokes.NilpotentVolterra.list_sum_eval {X : Type u_1} {E : Type u_2} [AddCommMonoid E] (l : List (X → E)) (x : X) : l.sum x = (List.map (fun (f : X → E) => f x) l).sum

theorem NavierStokes.NilpotentVolterra.norm_list_sum_le {E : Type u_1} [SeminormedAddCommGroup E] (l : List E) (M : ℝ) (h : ∀ x ∈ l, ‖x‖ ≤ M) : ‖l.sum‖ ≤ ↑l.length * M

theorem NavierStokes.NilpotentVolterra.holomorphic_list_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (l : List (ℂ → E)) {U : Set ℂ} (h : ∀ f ∈ l, DifferentiableOn ℂ f U) : DifferentiableOn ℂ l.sum U

noncomputable def NavierStokes.NilpotentVolterra.layer {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) (F : ℂ → Path R) (k : ℕ) : ℂ → Path R

Layer, given by ((binaryWords k).map (fun w => pathWord hR c A₀ A₁ w F)).sum.

Equations

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

theorem NavierStokes.NilpotentVolterra.layer_holomorphic {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) (k : ℕ) : DifferentiableOn ℂ (layer hR c A₀ A₁ F k) U

@[simp]

theorem NavierStokes.NilpotentVolterra.layer_zero {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) (F : ℂ → Path R) : layer hR c A₀ A₁ F 0 = F

theorem NavierStokes.NilpotentVolterra.pathLetter_add {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) (b : Bool) {F G : ℂ → Path R} {z : ℂ} (hF : DifferentiableAt ℂ F z) (hG : DifferentiableAt ℂ G z) : pathLetter hR c A₀ A₁ b (F + G) z = pathLetter hR c A₀ A₁ b F z + pathLetter hR c A₀ A₁ b G z

theorem NavierStokes.NilpotentVolterra.pathLetter_list_sum {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) (A₀ A₁ : ℂ → CoefficientPath R) (b : Bool) (l : List (ℂ → Path R)) {U : Set ℂ} (hU : IsOpen U) (h : ∀ F ∈ l, DifferentiableOn ℂ F U) {z : ℂ} (hz : z ∈ U) : (List.map (pathLetter hR c A₀ A₁ b) l).sum z = pathLetter hR c A₀ A₁ b l.sum z

theorem NavierStokes.NilpotentVolterra.layer_succ {R : ℝ} (hR : 0 ≤ R) (c : Fin 6 → ℕ) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) (k : ℕ) {z : ℂ} (hz : z ∈ U) : layer hR c A₀ A₁ F (k + 1) z = pathLetter hR c A₀ A₁ false (layer hR c A₀ A₁ F k) z + pathLetter hR c A₀ A₁ true (layer hR c A₀ A₁ F k) z

theorem NavierStokes.NilpotentVolterra.rawField_bound {R : ℝ} (hR : 0 ≤ R) (F : ℂ → Path R) {center : ℂ} {ρ B : ℝ} (hF : ∀ z ∈ Metric.closedBall center ρ, ‖F z‖ ≤ B) : VolterraAnalyticBounds.RadialBound (rawField hR F) R center ρ B 0

theorem NavierStokes.NilpotentVolterra.rawCoefficient_bound {R : ℝ} (hR : 0 ≤ R) (A : ℂ → CoefficientPath R) {center : ℂ} {ρ M : ℝ} (hA : ∀ z ∈ Metric.closedBall center ρ, ‖A z‖ ≤ M) : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A) R center ρ (6 * M)

theorem NavierStokes.NilpotentVolterra.pathWord_bound {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) (w : List Bool) {z : ℂ} (hz : z ∈ Metric.closedBall center ρ) : ‖pathWord hR VolterraAnalyticBounds.exponent A₀ A₁ w F z‖ ≤ B * VolterraAnalyticBounds.wordMajorant (M * R) (max 1 (σ - ρ)⁻¹) w.length

theorem NavierStokes.NilpotentVolterra.layer_bound {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) (k : ℕ) {z : ℂ} (hz : z ∈ Metric.closedBall center ρ) : ‖layer hR VolterraAnalyticBounds.exponent A₀ A₁ F k z‖ ≤ B * 2 ^ k * VolterraAnalyticBounds.wordMajorant (M * R) (max 1 (σ - ρ)⁻¹) k

noncomputable def NavierStokes.NilpotentVolterra.solutionSeries {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (F : ℂ → Path R) : ℂ → Path R

Solution series, defined pointwise by ∑' k : ℕ, layer hR VolterraAnalyticBounds.exponent A₀ A₁ F k z.

Equations

• NavierStokes.NilpotentVolterra.solutionSeries hR A₀ A₁ F z = ∑' (k : ℕ), NavierStokes.NilpotentVolterra.layer hR NavierStokes.VolterraAnalyticBounds.exponent A₀ A₁ F k z

theorem NavierStokes.NilpotentVolterra.solutionSeries_hasSum {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) {z : ℂ} (hz : z ∈ Metric.closedBall center ρ) : HasSum (fun (k : ℕ) => layer hR VolterraAnalyticBounds.exponent A₀ A₁ F k z) (solutionSeries hR A₀ A₁ F z)

theorem NavierStokes.NilpotentVolterra.solutionSeries_holomorphic {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) : DifferentiableOn ℂ (solutionSeries hR A₀ A₁ F) (Metric.ball center ρ)

The infinite series is a holomorphic map into the space of actual continuous radial paths, with no smallness restriction on the coefficients.

theorem NavierStokes.NilpotentVolterra.solutionSeries_deriv_hasSum {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) {z : ℂ} (hz : z ∈ Metric.ball center ρ) : HasSum (fun (k : ℕ) => deriv (layer hR VolterraAnalyticBounds.exponent A₀ A₁ F k) z) (deriv (solutionSeries hR A₀ A₁ F) z)

Actual complex differentiation commutes with the convergent Volterra series.

theorem NavierStokes.NilpotentVolterra.solutionSeries_equation {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {F : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hF : DifferentiableOn ℂ F U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbF : ∀ z ∈ Metric.closedBall center σ, ‖F z‖ ≤ B) {z : ℂ} (hz : z ∈ Metric.ball center ρ) : solutionSeries hR A₀ A₁ F z = F z + (pathInverse hR VolterraAnalyticBounds.exponent) ((coefficientAction (A₀ z)) (solutionSeries hR A₀ A₁ F z) + (coefficientAction (A₁ z)) (deriv (solutionSeries hR A₀ A₁ F) z))

The convergent series solves the genuine integral equation. In particular, convergence is not merely convergence of unrelated scalar bounds.

noncomputable def NavierStokes.NilpotentVolterra.integralSolution {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f : ℂ → Path R) : ℂ → Path R

Canonical series with the actual integrated forcing as its initial layer.

Equations

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

theorem NavierStokes.NilpotentVolterra.integralSolution_spec {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {f : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) {center : ℂ} {ρ σ : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) : DifferentiableOn ℂ (integralSolution hR A₀ A₁ f) (Metric.ball center ρ) ∧ ∀ z ∈ Metric.ball center ρ, integralSolution hR A₀ A₁ f z = (pathInverse hR VolterraAnalyticBounds.exponent) (f z + ((coefficientAction (A₀ z)) (integralSolution hR A₀ A₁ f z) + (coefficientAction (A₁ z)) (deriv (integralSolution hR A₀ A₁ f) z)))

Compactness supplies all coefficient bounds. Thus the actual solution theorem assumes neither a word bound nor convergence of its defining series.

noncomputable def NavierStokes.NilpotentVolterra.rhsPath {R : ℝ} (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) (z : ℂ) : Path R

Rhs path, given by f z + (coefficientAction (A₀ z) (W z) + coefficientAction (A₁ z) (deriv W z)).

Equations

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

noncomputable def NavierStokes.NilpotentVolterra.liftedField {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) : VolterraAnalyticBounds.Field

An actual radial function extending the solved path. Its definition uses the regular integral even at the axis and beyond the path interval.

Equations

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

theorem NavierStokes.NilpotentVolterra.liftedField_hasDerivAt {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) (r : ℝ) (z : ℂ) (i : Fin 6) : HasDerivAt (fun (s : ℝ) => liftedField hR A₀ A₁ f W s z i) (extendPath hR (rhsPath A₀ A₁ f W z) r i - ↑(VolterraAnalyticBounds.exponent i) • weightedMean (VolterraAnalyticBounds.exponent i) (fun (s : ℝ) => extendPath hR (rhsPath A₀ A₁ f W z) s i) r) r

theorem NavierStokes.NilpotentVolterra.liftedField_derivative_continuous {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) (z : ℂ) (i : Fin 6) : Continuous (deriv fun (r : ℝ) => liftedField hR A₀ A₁ f W r z i)

theorem NavierStokes.NilpotentVolterra.liftedField_axis_zero {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) (z : ℂ) : liftedField hR A₀ A₁ f W 0 z = 0

theorem NavierStokes.NilpotentVolterra.liftedField_eq_trace {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {z : ℂ} (hW : W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) {r : ℝ} (hr : r ∈ Set.Icc 0 R) : liftedField hR A₀ A₁ f W r z = rawField hR W r z

noncomputable def NavierStokes.NilpotentVolterra.equationRHS (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

Equation RHS as an element of VolterraAnalyticBounds.Field.

Equations

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

noncomputable def NavierStokes.NilpotentVolterra.radialDeriv (W : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

Radial derivative, defined pointwise by deriv (fun s : ℝ => W s z i) r.

Equations

• NavierStokes.NilpotentVolterra.radialDeriv W r z i = deriv (fun (s : ℝ) => W s z i) r

structure NavierStokes.NilpotentVolterra.IsRegularSolution (R : ℝ) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : Prop

A genuine regular solution of the singular first-order system. Radial regularity here is C¹, stated through ordinary derivatives and their continuity.

• jointly_continuous : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc 0 R ×ˢ U)
• parameter_holomorphic (r : ℝ) : r ∈ Set.Icc 0 R → ∀ (i : Fin 6), DifferentiableOn ℂ (fun (z : ℂ) => W r z i) U
• radial_differentiable (z : ℂ) : z ∈ U → ∀ (i : Fin 6), Differentiable ℝ fun (r : ℝ) => W r z i
• radial_derivative_continuous (z : ℂ) : z ∈ U → ∀ (i : Fin 6), Continuous fun (r : ℝ) => radialDeriv W r z i
• axis_zero (z : ℂ) : z ∈ U → W 0 z = 0
• equation (r : ℝ) : r ∈ Set.Icc 0 R → r ≠ 0 → ∀ z ∈ U, ∀ (i : Fin 6), radialDeriv W r z i + (↑(VolterraAnalyticBounds.exponent i) / r) • W r z i = equationRHS A₀ A₁ f W r z i
• axis_derivative (z : ℂ) : z ∈ U → ∀ (i : Fin 6), radialDeriv W 0 z i = (1 / (↑(VolterraAnalyticBounds.exponent i) + 1)) • equationRHS A₀ A₁ f W 0 z i

theorem NavierStokes.NilpotentVolterra.liftedField_parameterDeriv {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {U : Set ℂ} (hU : IsOpen U) (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) {r : ℝ} (hr : r ∈ Set.Icc 0 R) {z : ℂ} (hz : z ∈ U) : VolterraAnalyticBounds.parameterDeriv (liftedField hR A₀ A₁ f W) r z = rawField hR (deriv W) r z

theorem NavierStokes.NilpotentVolterra.liftedField_holomorphic {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {U : Set ℂ} (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) {r : ℝ} (hr : r ∈ Set.Icc 0 R) (i : Fin 6) : DifferentiableOn ℂ (fun (z : ℂ) => liftedField hR A₀ A₁ f W r z i) U

theorem NavierStokes.NilpotentVolterra.liftedField_rhs {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {U : Set ℂ} (hU : IsOpen U) (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) {r : ℝ} (hr : r ∈ Set.Icc 0 R) {z : ℂ} (hz : z ∈ U) : extendPath hR (rhsPath A₀ A₁ f W z) r = equationRHS (rawCoefficient hR A₀) (rawCoefficient hR A₁) (rawField hR f) (liftedField hR A₀ A₁ f W) r z

theorem NavierStokes.NilpotentVolterra.liftedField_jointly_continuous {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {U : Set ℂ} (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) : ContinuousOn (fun (p : ℝ × ℂ) => liftedField hR A₀ A₁ f W p.1 p.2) (Set.Icc 0 R ×ˢ U)

theorem NavierStokes.NilpotentVolterra.liftedField_isRegularSolution {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → CoefficientPath R) (f W : ℂ → Path R) {U : Set ℂ} (hU : IsOpen U) (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W z)) : IsRegularSolution R U (rawCoefficient hR A₀) (rawCoefficient hR A₁) (rawField hR f) (liftedField hR A₀ A₁ f W)

theorem NavierStokes.NilpotentVolterra.exists_regular_solution {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {f : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) {center : ℂ} {ρ σ : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) : ∃ (W : VolterraAnalyticBounds.Field), IsRegularSolution R (Metric.ball center ρ) (rawCoefficient hR A₀) (rawCoefficient hR A₁) (rawField hR f) W

A regular solution on any prescribed finite radial interval. Only the parameter neighborhood is reduced; coefficient size places no upper bound on the length of the radial interval.

theorem NavierStokes.NilpotentVolterra.homogeneous_layer_eq {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {V : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hV : DifferentiableOn ℂ V U) (heq : ∀ z ∈ U, V z = (pathInverse hR VolterraAnalyticBounds.exponent) ((coefficientAction (A₀ z)) (V z) + (coefficientAction (A₁ z)) (deriv V z))) (k : ℕ) {z : ℂ} (hz : z ∈ U) : layer hR VolterraAnalyticBounds.exponent A₀ A₁ V k z = V z

theorem NavierStokes.NilpotentVolterra.homogeneous_zero_on_closedDisk {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {V : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hV : DifferentiableOn ℂ V U) {center : ℂ} {ρ σ B M : ℝ} (hDisk : Metric.closedBall center σ ⊆ U) (hgap : ρ < σ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (hbA₀ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₀) R center σ M) (hbA₁ : VolterraAnalyticBounds.MatrixBound (rawCoefficient hR A₁) R center σ M) (hbV : ∀ z ∈ Metric.closedBall center σ, ‖V z‖ ≤ B) (heq : ∀ z ∈ U, V z = (pathInverse hR VolterraAnalyticBounds.exponent) ((coefficientAction (A₀ z)) (V z) + (coefficientAction (A₁ z)) (deriv V z))) {z : ℂ} (hz : z ∈ Metric.closedBall center ρ) : V z = 0

theorem NavierStokes.NilpotentVolterra.homogeneous_solution_zero {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {V : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hV : DifferentiableOn ℂ V U) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (heq : ∀ z ∈ U, V z = (pathInverse hR VolterraAnalyticBounds.exponent) ((coefficientAction (A₀ z)) (V z) + (coefficientAction (A₁ z)) (deriv V z))) (z : ℂ) : z ∈ U → V z = 0

Local compact bounds and the convergent majorant force every holomorphic homogeneous zero-axis solution to vanish.

theorem NavierStokes.NilpotentVolterra.integral_solution_unique {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {f W₀ W₁ : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hW₀ : DifferentiableOn ℂ W₀ U) (hW₁ : DifferentiableOn ℂ W₁ U) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) (heq₀ : ∀ z ∈ U, W₀ z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W₀ z)) (heq₁ : ∀ z ∈ U, W₁ z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f W₁ z)) : Set.EqOn W₀ W₁ U

Uniqueness in the holomorphic continuous-path class, with all local growth bounds derived from compactness.

theorem NavierStokes.NilpotentVolterra.integralSolution_spec_open {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {f : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) : DifferentiableOn ℂ (integralSolution hR A₀ A₁ f) U ∧ ∀ z ∈ U, integralSolution hR A₀ A₁ f z = (pathInverse hR VolterraAnalyticBounds.exponent) (rhsPath A₀ A₁ f (integralSolution hR A₀ A₁ f) z)

The same canonical series works locally on every disk in an arbitrary open parameter domain. Consequently its values are holomorphic on that domain; uniform estimates are taken on smaller compact neighborhoods.

theorem NavierStokes.NilpotentVolterra.exists_regular_solution_open {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → CoefficientPath R} {f : ℂ → Path R} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (rawCoefficient hR A₁)) : ∃ (W : VolterraAnalyticBounds.Field), IsRegularSolution R U (rawCoefficient hR A₀) (rawCoefficient hR A₁) (rawField hR f) W

Existence on any finite radial interval and any open parameter neighborhood carrying the fixed holomorphic input data.

theorem NavierStokes.NilpotentVolterra.IsRegularSolution.axis_derivative_eq_forcing {R : ℝ} {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (hsol : IsRegularSolution R U A₀ A₁ f W) (hU : IsOpen U) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : radialDeriv W 0 z i = (1 / (↑(VolterraAnalyticBounds.exponent i) + 1)) • f 0 z i

Zero axis data make the axis derivative depend only on the given forcing.

noncomputable def NavierStokes.VolterraParity.paritySign (i : Fin 6) : ℂ

Parity sign, with branches according to i.val < 4.

Equations

• NavierStokes.VolterraParity.paritySign i = if ↑i < 4 then 1 else -1

noncomputable def NavierStokes.VolterraParity.parityVec : VolterraAnalyticBounds.Vec →L[ℂ] VolterraAnalyticBounds.Vec

Parity vector, given by ContinuousLinearMap.pi (fun i => paritySign i • ContinuousLinearMap.proj i).

Equations

• NavierStokes.VolterraParity.parityVec = ContinuousLinearMap.pi fun (i : Fin 6) => NavierStokes.VolterraParity.paritySign i • ContinuousLinearMap.proj i

@[simp]

theorem NavierStokes.VolterraParity.parityVec_apply (v : VolterraAnalyticBounds.Vec) (i : Fin 6) : parityVec v i = paritySign i * v i

@[simp]

theorem NavierStokes.VolterraParity.paritySign_mul_self (i : Fin 6) : paritySign i * paritySign i = 1

@[simp]

theorem NavierStokes.VolterraParity.parityVec_involutive (v : VolterraAnalyticBounds.Vec) : parityVec (parityVec v) = v

def NavierStokes.VolterraParity.CoefficientParityOn (S : Set ℝ) (U : Set ℂ) (A : VolterraAnalyticBounds.Coeff) : Prop

Coefficient parity on, given by ∀ r ∈ S, ∀ z ∈ U, ∀ i j, A (-r) z i j = -(paritySign i * paritySign j) * A r z i j.

Equations

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

def NavierStokes.VolterraParity.ForcingParityOn (S : Set ℝ) (U : Set ℂ) (f : VolterraAnalyticBounds.Field) : Prop

Forcing parity on, given by ∀ r ∈ S, ∀ z ∈ U, ∀ i, f (-r) z i = -(paritySign i) * f r z i.

Equations

• NavierStokes.VolterraParity.ForcingParityOn S U f = ∀ r ∈ S, ∀ z ∈ U, ∀ (i : Fin 6), f (-r) z i = -NavierStokes.VolterraParity.paritySign i * f r z i

def NavierStokes.VolterraParity.CoefficientParity (A : VolterraAnalyticBounds.Coeff) : Prop

Coefficient parity, given by ∀ r z i j, A (-r) z i j = -(paritySign i * paritySign j) * A r z i j.

Equations

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

def NavierStokes.VolterraParity.ForcingParity (f : VolterraAnalyticBounds.Field) : Prop

Forcing parity, given by ∀ r z i, f (-r) z i = -(paritySign i) * f r z i.

Equations

• NavierStokes.VolterraParity.ForcingParity f = ∀ (r : ℝ) (z : ℂ) (i : Fin 6), f (-r) z i = -NavierStokes.VolterraParity.paritySign i * f r z i

noncomputable def NavierStokes.VolterraParity.reflectField (W : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

Reflect field, defined pointwise by W (-r) z.

Equations

• NavierStokes.VolterraParity.reflectField W r z = W (-r) z

noncomputable def NavierStokes.VolterraParity.reflectCoeff (A : VolterraAnalyticBounds.Coeff) : VolterraAnalyticBounds.Coeff

Reflect coefficient, defined pointwise by -A (-r) z.

Equations

• NavierStokes.VolterraParity.reflectCoeff A r z = -A (-r) z

noncomputable def NavierStokes.VolterraParity.reflectedForcing (f : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

Reflected forcing, defined pointwise by -f (-r) z.

Equations

• NavierStokes.VolterraParity.reflectedForcing f r z = -f (-r) z

@[simp]

theorem NavierStokes.VolterraParity.reflectField_twice (W : VolterraAnalyticBounds.Field) : reflectField (reflectField W) = W

@[simp]

theorem NavierStokes.VolterraParity.reflectCoeff_twice (A : VolterraAnalyticBounds.Coeff) : reflectCoeff (reflectCoeff A) = A

@[simp]

theorem NavierStokes.VolterraParity.reflectedForcing_twice (f : VolterraAnalyticBounds.Field) : reflectedForcing (reflectedForcing f) = f

@[simp]

theorem NavierStokes.VolterraParity.parameterDeriv_reflect (W : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.parameterDeriv (reflectField W) = reflectField (VolterraAnalyticBounds.parameterDeriv W)

theorem NavierStokes.VolterraParity.equationRHS_reflect (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : NilpotentVolterra.equationRHS (reflectCoeff A₀) (reflectCoeff A₁) (reflectedForcing f) (reflectField W) = reflectedForcing (NilpotentVolterra.equationRHS A₀ A₁ f W)

theorem NavierStokes.VolterraParity.radialInverse_reflect (F : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.radialInverse (reflectedForcing F) = reflectField (VolterraAnalyticBounds.radialInverse F)

The sign from radial reflection is exactly the sign in the reflected forcing. This is an identity of actual Bochner integrals.

theorem NavierStokes.VolterraParity.radialInverse_equationRHS_reflect (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.radialInverse (NilpotentVolterra.equationRHS (reflectCoeff A₀) (reflectCoeff A₁) (reflectedForcing f) (reflectField W)) = reflectField (VolterraAnalyticBounds.radialInverse (NilpotentVolterra.equationRHS A₀ A₁ f W))

def NavierStokes.VolterraParity.IntegralEquationOn (S : Set ℝ) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : Prop

The actual regular integral equation on a specified radial set.

Equations

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

theorem NavierStokes.VolterraParity.IntegralEquationOn.reflect {S : Set ℝ} {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (h : IntegralEquationOn S U A₀ A₁ f W) : IntegralEquationOn {r : ℝ | -r ∈ S} U (reflectCoeff A₀) (reflectCoeff A₁) (reflectedForcing f) (reflectField W)

theorem NavierStokes.VolterraParity.negativeHalf_equation {R : ℝ} {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W : VolterraAnalyticBounds.Field} (h : IntegralEquationOn (Set.Icc 0 R) U (reflectCoeff A₀) (reflectCoeff A₁) (reflectedForcing f) W) : IntegralEquationOn (Set.Icc (-R) 0) U A₀ A₁ f (reflectField W)

noncomputable def NavierStokes.VolterraParity.glue (Wp Wm : VolterraAnalyticBounds.Field) : VolterraAnalyticBounds.Field

Glue, defined pointwise by if 0 ≤ r then Wp r z else Wm (-r) z.

Equations

• NavierStokes.VolterraParity.glue Wp Wm r z = if 0 ≤ r then Wp r z else Wm (-r) z

theorem NavierStokes.VolterraParity.glue_nonneg (Wp Wm : VolterraAnalyticBounds.Field) {r : ℝ} (hr : 0 ≤ r) (z : ℂ) : glue Wp Wm r z = Wp r z

theorem NavierStokes.VolterraParity.glue_nonpos {Wp Wm : VolterraAnalyticBounds.Field} (h0 : ∀ (z : ℂ), Wp 0 z = Wm 0 z) {r : ℝ} (hr : r ≤ 0) (z : ℂ) : glue Wp Wm r z = Wm (-r) z

theorem NavierStokes.VolterraParity.equationRHS_congr_at {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f W V : VolterraAnalyticBounds.Field} {r : ℝ} (h : ∀ (z : ℂ), W r z = V r z) (z : ℂ) : NilpotentVolterra.equationRHS A₀ A₁ f W r z = NilpotentVolterra.equationRHS A₀ A₁ f V r z

theorem NavierStokes.VolterraParity.radialInverse_congr_at {F G : VolterraAnalyticBounds.Field} {r : ℝ} {z : ℂ} (h : ∀ t ∈ Set.Icc 0 1, F (t * r) z = G (t * r) z) : VolterraAnalyticBounds.radialInverse F r z = VolterraAnalyticBounds.radialInverse G r z

theorem NavierStokes.VolterraParity.glue_integralEquation {R : ℝ} {U : Set ℂ} {A₀ A₁ : VolterraAnalyticBounds.Coeff} {f Wp Wm : VolterraAnalyticBounds.Field} (h0 : ∀ (z : ℂ), Wp 0 z = Wm 0 z) (hp : IntegralEquationOn (Set.Icc 0 R) U A₀ A₁ f Wp) (hm : IntegralEquationOn (Set.Icc 0 R) U (reflectCoeff A₀) (reflectCoeff A₁) (reflectedForcing f) Wm) : IntegralEquationOn (Set.Icc (-R) R) U A₀ A₁ f (glue Wp Wm)

Gluing solves the equation on the entire symmetric interval. Equality of the axis traces is the only matching fact needed for this identity.

theorem NavierStokes.VolterraParity.glue_parameter_holomorphic {R : ℝ} {U : Set ℂ} {Wp Wm : VolterraAnalyticBounds.Field} (hp : ∀ r ∈ Set.Icc 0 R, ∀ (i : Fin 6), DifferentiableOn ℂ (fun (z : ℂ) => Wp r z i) U) (hm : ∀ r ∈ Set.Icc 0 R, ∀ (i : Fin 6), DifferentiableOn ℂ (fun (z : ℂ) => Wm r z i) U) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) (i : Fin 6) : DifferentiableOn ℂ (fun (z : ℂ) => glue Wp Wm r z i) U

theorem NavierStokes.VolterraParity.glue_jointly_continuous {R : ℝ} {U : Set ℂ} {Wp Wm : VolterraAnalyticBounds.Field} (h0 : ∀ z ∈ U, Wp 0 z = Wm 0 z) (hp : ContinuousOn (fun (p : ℝ × ℂ) => Wp p.1 p.2) (Set.Icc 0 R ×ˢ U)) (hm : ContinuousOn (fun (p : ℝ × ℂ) => Wm p.1 p.2) (Set.Icc 0 R ×ˢ U)) : ContinuousOn (fun (p : ℝ × ℂ) => glue Wp Wm p.1 p.2) (Set.Icc (-R) R ×ˢ U)

structure NavierStokes.VolterraParity.IsSymmetricIntegralSolution (R : ℝ) (U : Set ℂ) (A₀ A₁ : VolterraAnalyticBounds.Coeff) (f W : VolterraAnalyticBounds.Field) : Prop

The symmetric regular integral solution, before the radial smoothness bootstrap. No differentiability at the glued axis is assumed.

• jointly_continuous : ContinuousOn (fun (p : ℝ × ℂ) => W p.1 p.2) (Set.Icc (-R) R ×ˢ U)
• parameter_holomorphic (r : ℝ) : r ∈ Set.Icc (-R) R → ∀ (i : Fin 6), DifferentiableOn ℂ (fun (z : ℂ) => W r z i) U
• integral_equation : IntegralEquationOn (Set.Icc (-R) R) U A₀ A₁ f W
• axis_zero (z : ℂ) : z ∈ U → W 0 z = 0

@[reducible, inline]

abbrev NavierStokes.VolterraParity.SymmetricPath (R : ℝ) (E : Type u_1) [TopologicalSpace E] : Type u_1

Symmetric path: an abbreviation for C(Icc (-R) R, E).

Equations

• NavierStokes.VolterraParity.SymmetricPath R E = C(↑(Set.Icc (-R) R), E)

@[reducible, inline]

abbrev NavierStokes.VolterraParity.SymmetricCoefficientPath (R : ℝ) : Type

Symmetric coefficient path: an abbreviation for SymmetricPath R (Vec →L[ℂ] Vec).

Equations

• NavierStokes.VolterraParity.SymmetricCoefficientPath R = NavierStokes.VolterraParity.SymmetricPath R (NavierStokes.VolterraAnalyticBounds.Vec →L[ℂ] NavierStokes.VolterraAnalyticBounds.Vec)

noncomputable def NavierStokes.VolterraParity.positiveEmbedding {R : ℝ} (hR : 0 ≤ R) : C(↑(Set.Icc 0 R), ↑(Set.Icc (-R) R))

Positive embedding, given by ⟨fun x => ⟨x.1, ⟨(neg_nonpos.mpr hR).trans x.2.1, x.2.2⟩⟩, continuous_subtype_val.subtype_mk _⟩.

Equations

• NavierStokes.VolterraParity.positiveEmbedding hR = { toFun := fun (x : ↑(Set.Icc 0 R)) => ⟨↑x, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def NavierStokes.VolterraParity.negativeEmbedding {R : ℝ} (hR : 0 ≤ R) : C(↑(Set.Icc 0 R), ↑(Set.Icc (-R) R))

Negative embedding, given by ⟨fun x => ⟨-x.1, ⟨neg_le_neg x.2.2, (neg_nonpos.mpr x.2.1).trans hR⟩⟩, continuous_subtype_val.neg.subtype_mk _⟩.

Equations

• NavierStokes.VolterraParity.negativeEmbedding hR = { toFun := fun (x : ↑(Set.Icc 0 R)) => ⟨-↑x, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def NavierStokes.VolterraParity.sideEmbedding {R : ℝ} (hR : 0 ≤ R) (b : Bool) : C(↑(Set.Icc 0 R), ↑(Set.Icc (-R) R))

Side embedding, with branches according to b.

Equations

• NavierStokes.VolterraParity.sideEmbedding hR b = if b = true then NavierStokes.VolterraParity.negativeEmbedding hR else NavierStokes.VolterraParity.positiveEmbedding hR

noncomputable def NavierStokes.VolterraParity.sideRestriction {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (b : Bool) : SymmetricPath R E →L[ℂ] C(↑(Set.Icc 0 R), E)

Side restriction, constructed using LinearMap.mkContinuous.

Equations

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

noncomputable def NavierStokes.VolterraParity.signedRestriction {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (b : Bool) : SymmetricPath R E →L[ℂ] C(↑(Set.Icc 0 R), E)

Signed restriction, given by (if b then (-1 : ℂ) else 1) • sideRestriction hR b.

Equations

• NavierStokes.VolterraParity.signedRestriction hR b = (if b = true then -1 else 1) • NavierStokes.VolterraParity.sideRestriction hR b

noncomputable def NavierStokes.VolterraParity.sideData {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (b : Bool) (F : ℂ → SymmetricPath R E) : ℂ → C(↑(Set.Icc 0 R), E)

Side data, defined pointwise by signedRestriction hR b (F z).

Equations

• NavierStokes.VolterraParity.sideData hR b F z = (NavierStokes.VolterraParity.signedRestriction hR b) (F z)

@[simp]

theorem NavierStokes.VolterraParity.sideData_false {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (F : ℂ → SymmetricPath R E) (z : ℂ) (x : ↑(Set.Icc 0 R)) : (sideData hR false F z) x = (F z) ((positiveEmbedding hR) x)

@[simp]

theorem NavierStokes.VolterraParity.sideData_true {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (F : ℂ → SymmetricPath R E) (z : ℂ) (x : ↑(Set.Icc 0 R)) : (sideData hR true F z) x = -(F z) ((negativeEmbedding hR) x)

theorem NavierStokes.VolterraParity.sideData_holomorphic {R : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (hR : 0 ≤ R) (b : Bool) {F : ℂ → SymmetricPath R E} {U : Set ℂ} (hF : DifferentiableOn ℂ F U) : DifferentiableOn ℂ (sideData hR b F) U

noncomputable def NavierStokes.VolterraParity.symmetricRawField {R : ℝ} (hR : 0 ≤ R) (F : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec) : VolterraAnalyticBounds.Field

Symmetric raw field, defined pointwise by F z (projIcc (-R) R (by linarith) r).

Equations

• NavierStokes.VolterraParity.symmetricRawField hR F r z = (F z) (Set.projIcc (-R) R ⋯ r)

noncomputable def NavierStokes.VolterraParity.symmetricRawCoefficient {R : ℝ} (hR : 0 ≤ R) (A : ℂ → SymmetricCoefficientPath R) : VolterraAnalyticBounds.Coeff

Symmetric raw coefficient, defined pointwise by LinearMap.toMatrix' (A z (projIcc (-R) R (by linarith) r)).toLinearMap.

Equations

• NavierStokes.VolterraParity.symmetricRawCoefficient hR A r z = LinearMap.toMatrix' ↑((A z) (Set.projIcc (-R) R ⋯ r))

theorem NavierStokes.VolterraParity.sideRawField_pos {R : ℝ} (hR : 0 ≤ R) (F : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec) {r : ℝ} (hr : r ∈ Set.Icc 0 R) (z : ℂ) : NilpotentVolterra.rawField hR (sideData hR false F) r z = symmetricRawField hR F r z

theorem NavierStokes.VolterraParity.sideRawField_neg {R : ℝ} (hR : 0 ≤ R) (F : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec) {r : ℝ} (hr : r ∈ Set.Icc 0 R) (z : ℂ) : NilpotentVolterra.rawField hR (sideData hR true F) r z = reflectedForcing (symmetricRawField hR F) r z

theorem NavierStokes.VolterraParity.sideRawCoefficient_pos {R : ℝ} (hR : 0 ≤ R) (A : ℂ → SymmetricCoefficientPath R) {r : ℝ} (hr : r ∈ Set.Icc 0 R) (z : ℂ) : NilpotentVolterra.rawCoefficient hR (sideData hR false A) r z = symmetricRawCoefficient hR A r z

theorem NavierStokes.VolterraParity.sideRawCoefficient_neg {R : ℝ} (hR : 0 ≤ R) (A : ℂ → SymmetricCoefficientPath R) {r : ℝ} (hr : r ∈ Set.Icc 0 R) (z : ℂ) : NilpotentVolterra.rawCoefficient hR (sideData hR true A) r z = reflectCoeff (symmetricRawCoefficient hR A) r z

theorem NavierStokes.VolterraParity.side_shape {R : ℝ} (hR : 0 ≤ R) {A : ℂ → SymmetricCoefficientPath R} (hA : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A)) (b : Bool) : VolterraAnalyticBounds.DerivativeShape (NilpotentVolterra.rawCoefficient hR (sideData hR b A))

theorem NavierStokes.VolterraParity.lifted_integralEquation {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → NilpotentVolterra.CoefficientPath R} {f W : ℂ → NilpotentVolterra.Path R} {U : Set ℂ} (hU : IsOpen U) (hWholo : DifferentiableOn ℂ W U) (hW : ∀ z ∈ U, W z = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) (NilpotentVolterra.rhsPath A₀ A₁ f W z)) : IntegralEquationOn (Set.Icc 0 R) U (NilpotentVolterra.rawCoefficient hR A₀) (NilpotentVolterra.rawCoefficient hR A₁) (NilpotentVolterra.rawField hR f) (NilpotentVolterra.liftedField hR A₀ A₁ f W)

The positive solver's lifted function satisfies the normalized integral equation, including its value at zero.

theorem NavierStokes.VolterraParity.positive_equation_change_data {R : ℝ} {U : Set ℂ} {A₀ A₁ B₀ B₁ : VolterraAnalyticBounds.Coeff} {f g W : VolterraAnalyticBounds.Field} (h : IntegralEquationOn (Set.Icc 0 R) U A₀ A₁ f W) (h₀ : ∀ r ∈ Set.Icc 0 R, ∀ z ∈ U, A₀ r z = B₀ r z) (h₁ : ∀ r ∈ Set.Icc 0 R, ∀ z ∈ U, A₁ r z = B₁ r z) (hf : ∀ r ∈ Set.Icc 0 R, ∀ z ∈ U, f r z = g r z) : IntegralEquationOn (Set.Icc 0 R) U B₀ B₁ g W

noncomputable def NavierStokes.VolterraParity.sideSolution {R : ℝ} (hR : 0 ≤ R) (b : Bool) (A₀ A₁ : ℂ → SymmetricCoefficientPath R) (f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec) : VolterraAnalyticBounds.Field

Side solution, constructed using NilpotentVolterra.liftedField.

Equations

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

noncomputable def NavierStokes.VolterraParity.symmetricSolution {R : ℝ} (hR : 0 ≤ R) (A₀ A₁ : ℂ → SymmetricCoefficientPath R) (f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec) : VolterraAnalyticBounds.Field

Two independently solved half-intervals are glued at their common zero axis trace. No parity of the output occurs in this definition.

Equations

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

theorem NavierStokes.VolterraParity.sideSolution_spec {R : ℝ} (hR : 0 ≤ R) (b : Bool) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) : NilpotentVolterra.IsRegularSolution R U (NilpotentVolterra.rawCoefficient hR (sideData hR b A₀)) (NilpotentVolterra.rawCoefficient hR (sideData hR b A₁)) (NilpotentVolterra.rawField hR (sideData hR b f)) (sideSolution hR b A₀ A₁ f) ∧ IntegralEquationOn (Set.Icc 0 R) U (NilpotentVolterra.rawCoefficient hR (sideData hR b A₀)) (NilpotentVolterra.rawCoefficient hR (sideData hR b A₁)) (NilpotentVolterra.rawField hR (sideData hR b f)) (sideSolution hR b A₀ A₁ f) ∧ ∀ (z : ℂ), sideSolution hR b A₀ A₁ f 0 z = 0

theorem NavierStokes.VolterraParity.symmetricSolution_spec {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) : IsSymmetricIntegralSolution R U (symmetricRawCoefficient hR A₀) (symmetricRawCoefficient hR A₁) (symmetricRawField hR f) (symmetricSolution hR A₀ A₁ f)

Actual existence on a symmetric radial interval. Only holomorphy in the parameter and continuity in the radial coordinate are used here.

theorem NavierStokes.VolterraParity.exists_symmetric_integral_solution {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) : ∃ (W : VolterraAnalyticBounds.Field), IsSymmetricIntegralSolution R U (symmetricRawCoefficient hR A₀) (symmetricRawCoefficient hR A₁) (symmetricRawField hR f) W

theorem NavierStokes.VolterraParity.reflected_matrix_parity {S : Set ℝ} {U : Set ℂ} {A : VolterraAnalyticBounds.Coeff} (hA : CoefficientParityOn S U A) {r : ℝ} (hr : r ∈ S) {z : ℂ} (hz : z ∈ U) (v : VolterraAnalyticBounds.Vec) : (reflectCoeff A r z).mulVec (parityVec v) = parityVec ((A r z).mulVec v)

theorem NavierStokes.VolterraParity.reflected_forcing_parity {S : Set ℝ} {U : Set ℂ} {f : VolterraAnalyticBounds.Field} (hf : ForcingParityOn S U f) {r : ℝ} (hr : r ∈ S) {z : ℂ} (hz : z ∈ U) : reflectedForcing f r z = parityVec (f r z)

noncomputable def NavierStokes.VolterraParity.parityPath (R : ℝ) : NilpotentVolterra.Path R →L[ℂ] NilpotentVolterra.Path R

Parity path, given by ContinuousLinearMap.compLeftContinuous ℂ (Icc (0 : ℝ) R) parityVec.

Equations

• NavierStokes.VolterraParity.parityPath R = ContinuousLinearMap.compLeftContinuous ℂ (↑(Set.Icc 0 R)) NavierStokes.VolterraParity.parityVec

@[simp]

theorem NavierStokes.VolterraParity.parityPath_apply {R : ℝ} (W : NilpotentVolterra.Path R) (r : ↑(Set.Icc 0 R)) : ((parityPath R) W) r = parityVec (W r)

@[simp]

theorem NavierStokes.VolterraParity.parityPath_involutive {R : ℝ} (W : NilpotentVolterra.Path R) : (parityPath R) ((parityPath R) W) = W

theorem NavierStokes.VolterraParity.parityPath_deriv {R : ℝ} {W : ℂ → NilpotentVolterra.Path R} {z : ℂ} (hW : DifferentiableAt ℂ W z) : deriv (fun (w : ℂ) => (parityPath R) (W w)) z = (parityPath R) (deriv W z)

theorem NavierStokes.VolterraParity.parityPath_inverse {R : ℝ} (hR : 0 ≤ R) (W : NilpotentVolterra.Path R) : (parityPath R) ((NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) W) = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) ((parityPath R) W)

The diagonal parity action commutes with the actual radial integral.

theorem NavierStokes.VolterraParity.sideData_coefficient_parity {R : ℝ} (hR : 0 ≤ R) {A : ℂ → SymmetricCoefficientPath R} {U : Set ℂ} (hA : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A)) {z : ℂ} (hz : z ∈ U) (r : ↑(Set.Icc 0 R)) (v : VolterraAnalyticBounds.Vec) : ((sideData hR true A z) r) (parityVec v) = parityVec (((sideData hR false A z) r) v)

theorem NavierStokes.VolterraParity.sideData_forcing_parity {R : ℝ} (hR : 0 ≤ R) {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) {z : ℂ} (hz : z ∈ U) (r : ↑(Set.Icc 0 R)) : (sideData hR true f z) r = parityVec ((sideData hR false f z) r)

theorem NavierStokes.VolterraParity.rhsPath_parity {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {W : ℂ → NilpotentVolterra.Path R} {U : Set ℂ} (hA₀ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₀)) (hA₁ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₁)) (hf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) {z : ℂ} (hz : z ∈ U) (hW : DifferentiableAt ℂ W z) : NilpotentVolterra.rhsPath (sideData hR true A₀) (sideData hR true A₁) (sideData hR true f) (fun (w : ℂ) => (parityPath R) (W w)) z = (parityPath R) (NilpotentVolterra.rhsPath (sideData hR false A₀) (sideData hR false A₁) (sideData hR false f) W z)

theorem NavierStokes.VolterraParity.parity_transforms_equation {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {W : ℂ → NilpotentVolterra.Path R} {U : Set ℂ} (hU : IsOpen U) (hW : DifferentiableOn ℂ W U) (hA₀ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₀)) (hA₁ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₁)) (hf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) (heq : ∀ z ∈ U, W z = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) (NilpotentVolterra.rhsPath (sideData hR false A₀) (sideData hR false A₁) (sideData hR false f) W z)) (z : ℂ) : z ∈ U → (parityPath R) (W z) = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) (NilpotentVolterra.rhsPath (sideData hR true A₀) (sideData hR true A₁) (sideData hR true f) (fun (w : ℂ) => (parityPath R) (W w)) z)

Parity transforms a solution of the positive equation into a solution of the reflected positive equation.

theorem NavierStokes.VolterraParity.side_curves_parity {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) (hpA₀ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₀)) (hpA₁ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₁)) (hpf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) : Set.EqOn (NilpotentVolterra.integralSolution hR (sideData hR true A₀) (sideData hR true A₁) (sideData hR true f)) (fun (z : ℂ) => (parityPath R) (NilpotentVolterra.integralSolution hR (sideData hR false A₀) (sideData hR false A₁) (sideData hR false f) z)) U

The half-interval solutions have the required relation by uniqueness of the genuine integral equation.

theorem NavierStokes.VolterraParity.sideSolution_parity {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) (hpA₀ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₀)) (hpA₁ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₁)) (hpf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) {r : ℝ} (hr : r ∈ Set.Icc 0 R) {z : ℂ} (hz : z ∈ U) : sideSolution hR true A₀ A₁ f r z = parityVec (sideSolution hR false A₀ A₁ f r z)

theorem NavierStokes.VolterraParity.symmetricSolution_parity {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) (hpA₀ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₀)) (hpA₁ : CoefficientParityOn (Set.Icc 0 R) U (symmetricRawCoefficient hR A₁)) (hpf : ForcingParityOn (Set.Icc 0 R) U (symmetricRawField hR f)) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) {z : ℂ} (hz : z ∈ U) : symmetricSolution hR A₀ A₁ f (-r) z = parityVec (symmetricSolution hR A₀ A₁ f r z)

The actual symmetric solution has the prescribed vector parity. The coefficient/source parity hypotheses are transformed through the integral equation, and equality follows from holomorphic uniqueness.

theorem NavierStokes.VolterraParity.symmetricSolution_parity_of_global {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) (hpA₀ : CoefficientParity (symmetricRawCoefficient hR A₀)) (hpA₁ : CoefficientParity (symmetricRawCoefficient hR A₁)) (hpf : ForcingParity (symmetricRawField hR f)) {r : ℝ} (hr : r ∈ Set.Icc (-R) R) {z : ℂ} (hz : z ∈ U) : symmetricSolution hR A₀ A₁ f (-r) z = parityVec (symmetricSolution hR A₀ A₁ f r z)

theorem NavierStokes.VolterraParity.first_components_even {W : VolterraAnalyticBounds.Field} {R : ℝ} {U : Set ℂ} (hW : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = parityVec (W r z)) (i : Fin 6) (hi : ↑i < 4) {z : ℂ} (hz : z ∈ U) (r : ℝ) : r ∈ Set.Ioo (-R) R → W (-r) z i = W r z i

This is the component form used by the smooth even-descent theorem.

theorem NavierStokes.VolterraParity.last_components_odd {W : VolterraAnalyticBounds.Field} {R : ℝ} {U : Set ℂ} (hW : ∀ r ∈ Set.Icc (-R) R, ∀ z ∈ U, W (-r) z = parityVec (W r z)) (i : Fin 6) (hi : 4 ≤ ↑i) {z : ℂ} (hz : z ∈ U) (r : ℝ) : r ∈ Set.Ioo (-R) R → W (-r) z i = -W r z i

theorem NavierStokes.VolterraParity.hasDerivAt_glue_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {v : E} (hf : HasDerivAt f v 0) (hg : HasDerivAt g v 0) (h0 : f 0 = g 0) : HasDerivAt (fun (r : ℝ) => if 0 ≤ r then f r else g r) v 0

Two derivatives with the same value and axis trace glue to an ordinary two-sided derivative.

theorem NavierStokes.VolterraParity.symmetricSolution_hasDerivAt_zero {R : ℝ} (hR : 0 ≤ R) {A₀ A₁ : ℂ → SymmetricCoefficientPath R} {f : ℂ → SymmetricPath R VolterraAnalyticBounds.Vec} {U : Set ℂ} (hU : IsOpen U) (hA₀ : DifferentiableOn ℂ A₀ U) (hA₁ : DifferentiableOn ℂ A₁ U) (hf : DifferentiableOn ℂ f U) (hshape : VolterraAnalyticBounds.DerivativeShape (symmetricRawCoefficient hR A₁)) {z : ℂ} (hz : z ∈ U) (i : Fin 6) : HasDerivAt (fun (r : ℝ) => symmetricSolution hR A₀ A₁ f r z i) ((1 / (↑(VolterraAnalyticBounds.exponent i) + 1)) • symmetricRawField hR f 0 z i) 0

The derivatives from both sides match at the axis. The value is determined by the forcing, with the exact singular-diagonal factor.

theorem NavierStokes.VolterraParity.glued_solution_unique {R : ℝ} (hR : 0 ≤ R) {U : Set ℂ} (hU : IsOpen U) {A₀ A₁ : Bool → ℂ → NilpotentVolterra.CoefficientPath R} {f W₀ W₁ : Bool → ℂ → NilpotentVolterra.Path R} (hA₀ : ∀ (b : Bool), DifferentiableOn ℂ (A₀ b) U) (hA₁ : ∀ (b : Bool), DifferentiableOn ℂ (A₁ b) U) (hW₀ : ∀ (b : Bool), DifferentiableOn ℂ (W₀ b) U) (hW₁ : ∀ (b : Bool), DifferentiableOn ℂ (W₁ b) U) (hshape : ∀ (b : Bool), VolterraAnalyticBounds.DerivativeShape (NilpotentVolterra.rawCoefficient hR (A₁ b))) (heq₀ : ∀ (b : Bool), ∀ z ∈ U, W₀ b z = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) (NilpotentVolterra.rhsPath (A₀ b) (A₁ b) (f b) (W₀ b) z)) (heq₁ : ∀ (b : Bool), ∀ z ∈ U, W₁ b z = (NilpotentVolterra.pathInverse hR VolterraAnalyticBounds.exponent) (NilpotentVolterra.rhsPath (A₀ b) (A₁ b) (f b) (W₁ b) z)) (r : ℝ) {z : ℂ} (hz : z ∈ U) : glue (NilpotentVolterra.liftedField hR (A₀ false) (A₁ false) (f false) (W₀ false)) (NilpotentVolterra.liftedField hR (A₀ true) (A₁ true) (f true) (W₀ true)) r z = glue (NilpotentVolterra.liftedField hR (A₀ false) (A₁ false) (f false) (W₁ false)) (NilpotentVolterra.liftedField hR (A₀ true) (A₁ true) (f true) (W₁ true)) r z

Uniqueness of the glued actual lifts in the holomorphic path class. Both sides are compared by the proved positive Volterra uniqueness theorem; no uniqueness premise is introduced.