MetricCoercivity.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Coercive Jacobians and changes of frozen metric

A lower metric estimate gives injectivity, hence an invertible Jacobian in finite dimension. Taking the adjoint of T ∘ e.symm controls the inverse transpose in the frozen dual norm, with no condition-number loss.

theorem OAI.RegularPointCoordinates.norm_le_sqrt_mul_of_metric_lower line 23

Source documentation

The square-root form of the lower metric estimate.

theorem norm_le_sqrt_mul_of_metric_lower (T : E ≃L[ℝ] E) (J : E →L[ℝ] E)
    {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2) (xi : E) :
    ‖T xi‖ ≤ Real.sqrt A * ‖J xi‖ := by
…

theorem OAI.RegularPointCoordinates.injective_of_metric_lower line 38

Source documentation

A coercive Jacobian has trivial kernel, in any normed dimension.

theorem injective_of_metric_lower (T : E ≃L[ℝ] E) (J : E →L[ℝ] E)
    {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2) :
    Function.Injective J := by
…

theorem OAI.RegularPointCoordinates.exists_equiv_of_metric_lower line 53

Source documentation

In finite dimension the lower metric bound supplies the actual continuous linear equivalence representing the Jacobian.

theorem exists_equiv_of_metric_lower [FiniteDimensional ℝ E]
    (T : E ≃L[ℝ] E) (J : E →L[ℝ] E) {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2) :
    ∃ e : E ≃L[ℝ] E, (e : E →L[ℝ] E) = J := by
…

theorem OAI.RegularPointCoordinates.isUnit_of_metric_lower line 65

Source documentation

The same construction supplies the unit premise used by the inverse derivative lemmas.

theorem isUnit_of_metric_lower [FiniteDimensional ℝ E]
    (T : E ≃L[ℝ] E) (J : E →L[ℝ] E) {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2) : IsUnit J := by
…

theorem OAI.RegularPointCoordinates.norm_frozen_comp_inverse_le line 74

Source documentation

The inverse Jacobian has norm at most sqrt A when its output is measured using the frozen primal norm.

theorem norm_frozen_comp_inverse_le (T e : E ≃L[ℝ] E) {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖e xi‖ ^ 2) :
    ‖(T : E →L[ℝ] E) ∘L (e.symm : E →L[ℝ] E)‖ ≤ Real.sqrt A := by
…

theorem OAI.RegularPointCoordinates.norm_metric_change_le_one line 85

Source documentation

Increasing frozen metrics make the next-to-current coordinate map a contraction.

theorem norm_metric_change_le_one (Told Tnew : E ≃L[ℝ] E)
    (hmetric : ∀ xi, ‖Told xi‖ ≤ ‖Tnew xi‖) :
    ‖(Told : E →L[ℝ] E) ∘L (Tnew.symm : E →L[ℝ] E)‖ ≤ 1 := by
…

theorem OAI.RegularPointCoordinates.norm_metric_change_le_one_of_sq line 93

theorem OAI.RegularPointCoordinates.inverseTranspose_frozen_factor line 107

Source documentation

The inverse transpose factors through the frozen dual norm.

theorem inverseTranspose_frozen_factor (T e : E ≃L[ℝ] E) (w : E) :
    inverseTranspose e w =
      ((T : E →L[ℝ] E) ∘L (e.symm : E →L[ℝ] E)).adjoint
        ((T.symm : E →L[ℝ] E).adjoint w) := by
…

Mentions: OAI.RegularPointCoordinates.inverseTranspose

theorem OAI.RegularPointCoordinates.inverseTranspose_norm_le_frozen line 125

Source documentation

Lower metric coercivity gives the dual inverse-transpose bound with the same square-root constant.

theorem inverseTranspose_norm_le_frozen (T e : E ≃L[ℝ] E) {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖e xi‖ ^ 2) (w : E) :
    ‖inverseTranspose e w‖ ≤ Real.sqrt A * ‖(T.symm : E →L[ℝ] E).adjoint w‖ := by
…

Mentions: OAI.RegularPointCoordinates.inverseTranspose

theorem OAI.RegularPointCoordinates.exists_equiv_inverseTranspose_bound line 141

Source documentation

Existence and the dual estimate may be obtained together directly from the metric lower bound.

theorem exists_equiv_inverseTranspose_bound [FiniteDimensional ℝ E]
    (T : E ≃L[ℝ] E) (J : E →L[ℝ] E) {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2) :
    ∃ e : E ≃L[ℝ] E, (e : E →L[ℝ] E) = J ∧
      ∀ w, ‖inverseTranspose e w‖ ≤ Real.sqrt A * ‖(T.symm : E →L[ℝ] E).adjoint w‖ := by
…

Mentions: OAI.RegularPointCoordinates.inverseTranspose