Parameter regularity of the genuinely constructed coercive inverse

The positive lower-bound certificate may vary with the parameter and need not be differentiable. The inverse itself is the actual operator inverse, so its regularity depends only on the operator coefficients.

theorem EulerHilbertCoerciveParameter.contDiff_coerciveInverse_variable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → E →L[ℝ] E) (c : P → ℝ) (hc : ∀ (x : P), 0 < c x) (hA : ∀ (x : P) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) {n : WithTop ℕ∞} (hreg : ContDiff ℝ n A) : ContDiff ℝ n fun (x : P) => EulerCoerciveProjection.coerciveInverse (A x) (c x) ⋯ ⋯

Changing the coercivity certificate does not affect parameter regularity of the actual inverse operator.

theorem EulerHilbertCoerciveParameter.hasDerivAt_coerciveInverse_variable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (c : ℝ → ℝ) (hc : ∀ (x : ℝ), 0 < c x) (hA : ∀ (x : ℝ) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (x : ℝ) (A₁ : E →L[ℝ] E) (hder : HasDerivAt A A₁ x) : HasDerivAt (fun (r : ℝ) => EulerCoerciveProjection.coerciveInverse (A r) (c r) ⋯ ⋯) (-EulerCoerciveProjection.coerciveInverse (A x) (c x) ⋯ ⋯ ∘SL A₁ ∘SL EulerCoerciveProjection.coerciveInverse (A x) (c x) ⋯ ⋯) x

The actual derivative of an inverse, even with a varying coercivity certificate.

theorem EulerHilbertCoerciveParameter.contDiff_coerciveSolution_variable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → E →L[ℝ] E) (c : P → ℝ) (hc : ∀ (x : P), 0 < c x) (hA : ∀ (x : P) (v : E), c x * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : P → E) {n : WithTop ℕ∞} (hreg : ContDiff ℝ n A) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerCoerciveProjection.coerciveInverse (A x) (c x) ⋯ ⋯) (f x)

Actual forcing-to-solution regularity for a parameterized coercive solve.