WeightedInverse.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Inverse increments without commutation assumptions

The arguments use positive quadratic forms and exact inverse identities. Operators from different scales are never assumed to commute.

theorem OAI.RegularPointCoordinates.positive_equiv_symm line 21
Source documentation
Positivity is preserved by the inverse of a linear equivalence.
```
theorem positive_equiv_symm (Q : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) : (Q.symm : E →L[ℝ] E).IsPositive :=
…
```

theorem OAI.RegularPointCoordinates.inverse_increment_apply line 26

Source documentation

Exact resolvent identity evaluated on a vector.

theorem inverse_increment_apply (P Q : E ≃L[ℝ] E) (xi : E) :
    ((Q.symm : E →L[ℝ] E) - (P.symm : E →L[ℝ] E)) xi =
      Q.symm (((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)) (P.symm xi)) := by
…

theorem OAI.RegularPointCoordinates.inverse_increment_quadratic_identity line 34

Source documentation

The inverse increment equals the leading conjugated decrement plus a nonnegative remainder.

theorem inverse_increment_quadratic_identity (P Q : E ≃L[ℝ] E)
    (hP : (P : E →L[ℝ] E).IsPositive)
    (hD : ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)).IsPositive) (xi : E) :
    let D := (P : E →L[ℝ] E) - (Q : E →L[ℝ] E)
…

theorem OAI.RegularPointCoordinates.inverse_increment_order line 64

Source documentation

The sharp two-sided inverse-increment order for a relatively small positive decrement. This replaces the one-matrix spectral calculation.

theorem inverse_increment_order (P Q : E ≃L[ℝ] E)
    (hP : (P : E →L[ℝ] E).IsPositive) (hQ : (Q : E →L[ℝ] E).IsPositive)
    (hD : ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)).IsPositive)
    {eta : ℝ} (heta : 0 ≤ eta) (heta1 : eta < 1)
    (hsmall : ∀ v, ⟪v, ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)) v⟫_ℝ ≤
      eta * ⟪v, P v⟫_ℝ) (xi : E) :
    let D := (P : E →L[ℝ] E) - (Q : E →L[ℝ] E)
…

theorem OAI.RegularPointCoordinates.positive_inverse_sandwich_bound line 115

Source documentation

A positive form bounded by eta Q satisfies the weighted square bound D Q⁻¹ D ≤ eta D.

theorem positive_inverse_sandwich_bound (Q : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) {D : E →L[ℝ] E} (hD : D.IsPositive)
    {eta : ℝ} (heta : 0 ≤ eta)
    (hsmall : ∀ v, ⟪v, D v⟫_ℝ ≤ eta * ⟪v, Q v⟫_ℝ) (w : E) :
    ⟪D w, Q.symm (D w)⟫_ℝ ≤ eta * ⟪w, D w⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inverse_increment_isPositive line 141

Source documentation

A monotone positive metric sequence has positive inverse increments.

theorem inverse_increment_isPositive (P Q : E ≃L[ℝ] E)
    (hP : (P : E →L[ℝ] E).IsPositive) (hQ : (Q : E →L[ℝ] E).IsPositive)
    (hD : ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)).IsPositive) :
    ((Q.symm : E →L[ℝ] E) - (P.symm : E →L[ℝ] E)).IsPositive := by
…

theorem OAI.RegularPointCoordinates.inverse_increment_weighted_square_le line 158

Source documentation

For a half-small decrement the inverse increment satisfies the weighted square bound used in the convolution argument.

theorem inverse_increment_weighted_square_le (P Q : E ≃L[ℝ] E)
    (hP : (P : E →L[ℝ] E).IsPositive) (hQ : (Q : E →L[ℝ] E).IsPositive)
    (hD : ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)).IsPositive)
    (hsmall : ∀ v, ⟪v, ((P : E →L[ℝ] E) - (Q : E →L[ℝ] E)) v⟫_ℝ ≤
      (1 / 2 : ℝ) * ⟪v, P v⟫_ℝ) (xi : E) :
    let B := (Q.symm : E →L[ℝ] E) - (P.symm : E →L[ℝ] E)
…

theorem OAI.RegularPointCoordinates.inverse_energy_of_bilinear_bound line 184

Source documentation

The inverse-energy form of a bilinear comparison, obtained by testing at the actual inverse image rather than assuming a duality formula.

theorem inverse_energy_of_bilinear_bound (Q : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) (z : E) {K : ℝ} (hK : 0 ≤ K)
    (hbound : ∀ v, ⟪v, z⟫_ℝ ^ 2 ≤ K * ⟪v, Q v⟫_ℝ) :
    ⟪z, Q.symm z⟫_ℝ ≤ K := by
…

theorem OAI.RegularPointCoordinates.relative_inverse_bounds line 203

Source documentation

Relative comparison of positive metrics gives both inverse order and the weighted inverse-square estimate needed for normalization errors.

theorem relative_inverse_bounds (Q R : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) (hR : (R : E →L[ℝ] E).IsPositive)
    {c : ℝ} (hc : 0 < c)
    (hcompare : ∀ v, c * ⟪v, Q v⟫_ℝ ≤ ⟪v, R v⟫_ℝ) (z : E) :
    ⟪z, R.symm z⟫_ℝ ≤ ⟪z, Q.symm z⟫_ℝ / c ∧
      ⟪R.symm z, Q (R.symm z)⟫_ℝ ≤ ⟪z, Q.symm z⟫_ℝ / c ^ 2 := by
…

theorem OAI.RegularPointCoordinates.inverse_normalization_error_identity line 249

Source documentation

Exact change of inverse normalization.

theorem inverse_normalization_error_identity (Q R : E ≃L[ℝ] E) (xi : E) :
    R.symm xi - Q.symm xi =
      -(R.symm (((R : E →L[ℝ] E) - (Q : E →L[ℝ] E)) (Q.symm xi))) := by
…

theorem OAI.RegularPointCoordinates.inverse_normalization_error_le line 258

Source documentation

Bilinear heat comparison and relative metric comparison imply the normalization-error bound. Neither inverse order nor the error is assumed.

theorem inverse_normalization_error_le (Q R : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) (hR : (R : E →L[ℝ] E).IsPositive)
    (F : E →L[ℝ] E) (hF : F.IsPositive) {c C : ℝ} (hc : 0 < c) (hC : 0 ≤ C)
    (hcompare : ∀ v, c * ⟪v, Q v⟫_ℝ ≤ ⟪v, R v⟫_ℝ)
    (hbilinear : ∀ u v,
      ⟪v, ((R : E →L[ℝ] E) - (Q : E →L[ℝ] E)) u⟫_ℝ ^ 2 ≤
        (C * ⟪u, F u⟫_ℝ) * ⟪v, Q v⟫_ℝ) (xi : E) :
    ⟪R.symm xi - Q.symm xi, Q (R.symm xi - Q.symm xi)⟫_ℝ ≤
      C / c ^ 2 * ⟪Q.symm xi, F (Q.symm xi)⟫_ℝ := by
…