HessianCoercivity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.bilinear_coercive_of_norm_sub_le line 14

Source documentation

A quantitative lower bound on a bilinear form survives a small operator-norm perturbation. No finite-dimensional hypothesis is needed.

theorem bilinear_coercive_of_norm_sub_le
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (B C : E →L[ℝ] E →L[ℝ] ℝ) (a δ : ℝ)
    (hB : ∀ v, a * ‖v‖ ^ 2 ≤ B v v) (hclose : ‖C - B‖ ≤ δ) :
    ∀ v, (a - δ) * ‖v‖ ^ 2 ≤ C v v := by
…

theorem OAI.Problem356.eventually_bilinear_coercive line 33

Source documentation

A continuous family of coercive bilinear forms remains uniformly coercive near the base point, with half the original lower-bound constant.

theorem eventually_bilinear_coercive
    {X : Type uX} {E : Type uE} [TopologicalSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (B : X → E →L[ℝ] E →L[ℝ] ℝ) (x₀ : X) (a : ℝ)
    (ha : 0 < a) (hcont : ContinuousAt B x₀)
    (hbase : ∀ v, a * ‖v‖ ^ 2 ≤ B x₀ v v) :
    ∀ᶠ x in 𝓝 x₀, ∀ v, (a / 2) * ‖v‖ ^ 2 ≤ B x v v := by
…

theorem OAI.Problem356.exists_bilinear_coercivity_of_pos line 50

Source documentation

In finite dimension, strict positivity of a continuous bilinear form gives one uniform positive quadratic lower bound.

theorem exists_bilinear_coercivity_of_pos
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    (B : E →L[ℝ] E →L[ℝ] ℝ) (hpos : ∀ v, v ≠ 0 → 0 < B v v) :
    ∃ a : ℝ, 0 < a ∧ ∀ v, a * ‖v‖ ^ 2 ≤ B v v := by
…

theorem OAI.Problem356.eventually_bilinear_pos line 87

Source documentation

Positive definiteness is an open condition for continuous bilinear families on finite-dimensional real normed spaces.

theorem eventually_bilinear_pos
    {X : Type uX} {E : Type uE} [TopologicalSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (B : X → E →L[ℝ] E →L[ℝ] ℝ) (x₀ : X)
    (hcont : ContinuousAt B x₀) (hpos : ∀ v, v ≠ 0 → 0 < B x₀ v v) :
    ∀ᶠ x in 𝓝 x₀, ∀ v, v ≠ 0 → 0 < B x v v := by
…

theorem OAI.Problem356.exists_ball_bilinear_pos line 99

Source documentation

Metric-ball version of openness of positive definiteness.

theorem exists_ball_bilinear_pos
    {X : Type uX} {E : Type uE} [PseudoMetricSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (B : X → E →L[ℝ] E →L[ℝ] ℝ) (x₀ : X)
    (hcont : ContinuousAt B x₀) (hpos : ∀ v, v ≠ 0 → 0 < B x₀ v v) :
    ∃ r : ℝ, 0 < r ∧ ∀ x ∈ Metric.ball x₀ r, ∀ v, v ≠ 0 → 0 < B x v v := by
…

theorem OAI.Problem356.exists_ball_hessian_pos line 110

Source documentation

A positive-definite Hessian at a point stays positive definite on a ball when the function is twice continuously differentiable there.

theorem exists_ball_hessian_pos
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    (f : E → ℝ) (x₀ : E) (hf : ContDiffAt ℝ 2 f x₀)
    (hpos : ∀ v, v ≠ 0 → 0 < fderiv ℝ (fderiv ℝ f) x₀ v v) :
    ∃ r : ℝ, 0 < r ∧ ∀ x ∈ Metric.ball x₀ r, ∀ v, v ≠ 0 →
      0 < fderiv ℝ (fderiv ℝ f) x v v := by
…