Smooth dependence of quadratic moment repair

The coefficients of a quadratic moment map are included among the variables of a universal polynomial map. Its derivative at zero correction is a proved product equivalence. The smooth inverse-function theorem constructs a local solver; no solution branch or its regularity is assumed.

@[reducible, inline]

abbrev NavierStokes.SmoothMomentRepair.QuadraticCoefficients (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_1

Quadratic coefficients: an abbreviation for (E →L[ℝ] E) × (E →L[ℝ] E →L[ℝ] E).

Equations

• NavierStokes.SmoothMomentRepair.QuadraticCoefficients E = ((E →L[ℝ] E) × (E →L[ℝ] E →L[ℝ] E))

@[reducible, inline]

abbrev NavierStokes.SmoothMomentRepair.RepairData (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_1

Repair data: an abbreviation for QuadraticCoefficients E × E.

Equations

• NavierStokes.SmoothMomentRepair.RepairData E = (NavierStokes.SmoothMomentRepair.QuadraticCoefficients E × E)

noncomputable def NavierStokes.SmoothMomentRepair.forward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : RepairData E) : RepairData E

The same type holds an unknown correction on input and a moment debt on output.

Equations

• NavierStokes.SmoothMomentRepair.forward z = (z.1, z.1.1 z.2 + (z.1.2 z.2) z.2)

def NavierStokes.SmoothMomentRepair.base {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) : RepairData E

Base, given by ((B.toContinuousLinearMap, A), 0).

Equations

• NavierStokes.SmoothMomentRepair.base B A = ((↑B, A), 0)

theorem NavierStokes.SmoothMomentRepair.forward_base {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) : forward (base B A) = base B A

theorem NavierStokes.SmoothMomentRepair.forward_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : ContDiff ℝ ⊤ forward

This universal coefficient map is polynomial, hence analytic.

theorem NavierStokes.SmoothMomentRepair.forward_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) : HasFDerivAt forward (↑((ContinuousLinearEquiv.refl ℝ (QuadraticCoefficients E)).prodCongr B)) (base B A)

Invertibility of the full product derivative is derived from the linear part alone.

theorem NavierStokes.SmoothMomentRepair.exists_local_analytic_solver {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) : ∃ (g : RepairData E → E) (U : Set (RepairData E)), IsOpen U ∧ base B A ∈ U ∧ ContDiffOn ℝ ⊤ g U ∧ g (base B A) = 0 ∧ ∀ z ∈ U, z.1.1 (g z) + (z.1.2 (g z)) (g z) = z.2

A common open neighborhood supports an analytic solution in all coefficients and the debt.

theorem NavierStokes.SmoothMomentRepair.solution_norm_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B₀ : E ≃L[ℝ] E) (B : E →L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (c d : E) (β δ K r : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hinv : ∀ (x : E), ‖B₀.symm x‖ ≤ β * ‖x‖) (hB : ‖B - ↑B₀‖ ≤ δ) (hA : ‖A‖ ≤ K) (hc : ‖c‖ ≤ r) (hsmall : β * (δ + K * r) ≤ 1 / 2) (heq : B c + (A c) c = d) : ‖c‖ ≤ 2 * β * ‖d‖

A quantitative bound derived by absorbing both the linear perturbation and the quadratic term.

theorem NavierStokes.SmoothMomentRepair.exists_local_bounded_analytic_solver {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (B₀ : E ≃L[ℝ] E) (A₀ : E →L[ℝ] E →L[ℝ] E) : ∃ (g : RepairData E → E) (U : Set (RepairData E)) (C : ℝ), IsOpen U ∧ base B₀ A₀ ∈ U ∧ 0 < C ∧ ContDiffOn ℝ ⊤ g U ∧ g (base B₀ A₀) = 0 ∧ ∀ z ∈ U, z.1.1 (g z) + (z.1.2 (g z)) (g z) = z.2 ∧ ‖g z‖ ≤ C * ‖z.2‖

The analytic solver has a uniform linear-in-debt bound on one common open neighborhood.

theorem NavierStokes.SmoothMomentRepair.exists_smooth_parameter_branch {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (p₀ : P) (B : P → E →L[ℝ] E) (A : P → E →L[ℝ] E →L[ℝ] E) (d : P → E) (hB : ContDiff ℝ (↑⊤) B) (hA : ContDiff ℝ (↑⊤) A) (hd : ContDiff ℝ (↑⊤) d) (B₀ : E ≃L[ℝ] E) (hB₀ : B p₀ = ↑B₀) (hd₀ : d p₀ = 0) : ∃ (c : P → E) (U : Set P) (C : ℝ), IsOpen U ∧ p₀ ∈ U ∧ 0 < C ∧ ContDiffOn ℝ (↑⊤) c U ∧ c p₀ = 0 ∧ ∀ p ∈ U, (B p) (c p) + ((A p) (c p)) (c p) = d p ∧ ‖c p‖ ≤ C * ‖d p‖

Smooth coefficient and debt families produce a genuinely smooth exact small branch.

theorem NavierStokes.SmoothMomentRepair.quadratic_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] E →L[ℝ] E) (c : E) : ‖(A c) c‖ ≤ ‖A‖ * ‖c‖ ^ 2

The quadratic growth constant is the actual norm of the bilinear coefficient.

theorem NavierStokes.SmoothMomentRepair.quadratic_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] E →L[ℝ] E) (c e : E) : ‖(A c) c - (A e) e‖ ≤ ‖A‖ * (‖c‖ + ‖e‖) * ‖c - e‖

The two-point quadratic estimate follows from bilinearity.

theorem NavierStokes.SmoothMomentRepair.exists_unique_quadratic_correction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (B : E ≃L[ℝ] E) (A : E →L[ℝ] E →L[ℝ] E) (d : E) (r : ℝ) (hr : 0 ≤ r) (hsmall : 4 * ‖↑B.symm‖ * ‖A‖ * r ≤ 1) (hd : 2 * ‖↑B.symm‖ * ‖d‖ ≤ r) : ∃! c : E, ‖c‖ ≤ r ∧ B c + (A c) c = d

The existing contraction theorem gives uniqueness in the quantitative correction ball, with all quadratic estimates proved from the supplied coefficients.

theorem NavierStokes.SmoothMomentRepair.compact_inverse_quadratic_bounds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [TopologicalSpace P] (S : Set P) (hS : IsCompact S) (B : P → E →L[ℝ] E) (A : P → E →L[ℝ] E →L[ℝ] E) (hB : ContinuousOn B S) (hA : ContinuousOn A S) (hinv : ∀ p ∈ S, (B p).IsInvertible) : ∃ (β : ℝ) (K : ℝ), 0 < β ∧ 0 < K ∧ ∀ p ∈ S, ‖(B p).inverse‖ ≤ β ∧ ‖A p‖ ≤ K

Compactness supplies genuine uniform bounds on the inverse linear part and the quadratic coefficient; these bounds are not additional hypotheses.

theorem NavierStokes.SmoothMomentRepair.compact_uniform_small_correction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [TopologicalSpace P] (S : Set P) (hS : IsCompact S) (B : P → E →L[ℝ] E) (A : P → E →L[ℝ] E →L[ℝ] E) (hB : ContinuousOn B S) (hA : ContinuousOn A S) (hinv : ∀ p ∈ S, (B p).IsInvertible) : ∃ (β : ℝ) (ε : ℝ), 0 < β ∧ 0 < ε ∧ ∀ p ∈ S, ∀ (d : E), ‖d‖ ≤ ε → ∃! c : E, ‖c‖ ≤ 2 * β * ‖d‖ ∧ (B p) c + ((A p) c) c = d

A common positive discrepancy threshold and linear correction bound exist for every continuous invertible quadratic family on a compact parameter set.