FrozenNorms.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Frozen primal and dual norms

A continuous linear equivalence T represents the frozen square root of the source metric. The primal norm is ‖T x‖, and the dual norm is ‖(T.symm).adjoint w‖. Congruence by the inverse of T transports the positive-form bounds to Euclidean norms without a condition-number loss. No construction or differentiation of a matrix square root is required.

def OAI.RegularPointCoordinates.frozenConjugate line 24
Source documentation
A covariant positive form in frozen Euclidean coordinates.
```
def frozenConjugate (T : E ≃L[ℝ] E) (D : E →L[ℝ] E) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.inner_frozenConjugate line 27
theorem OAI.RegularPointCoordinates.frozenConjugate_apply_primal line 33
theorem OAI.RegularPointCoordinates.frozenConjugate_isPositive line 38
Source documentation
Congruence preserves positivity even when the mass form is singular.
```
theorem frozenConjugate_isPositive (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) : (frozenConjugate T D).IsPositive :=
…
```
Mentions: OAI.RegularPointCoordinates.frozenConjugate

theorem OAI.RegularPointCoordinates.frozenConjugate_form_bound line 43

Source documentation

A bound by the frozen source metric becomes a Euclidean form bound.

theorem frozenConjugate_form_bound (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    {epsilon : ℝ} (hbound : ∀ x, ⟪x, D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) (z : E) :
    ⟪z, frozenConjugate T D z⟫_ℝ ≤ epsilon * ‖z‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.frozenConjugate

theorem OAI.RegularPointCoordinates.frozen_positive_form_norm_sq_le line 51

Source documentation

The sharp anisotropic positive-matrix estimate: the dual norm of D w is controlled by its own directional mass, not by the full metric.

theorem frozen_positive_form_norm_sq_le (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) {epsilon : ℝ}
    (hbound : ∀ x, ⟪x, D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) (w : E) :
    ‖(T.symm : E →L[ℝ] E).adjoint (D w)‖ ^ 2 ≤ epsilon * ⟪w, D w⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.frozen_positive_form_norm_le line 61

Source documentation

The same estimate in square-root form.

theorem frozen_positive_form_norm_le (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hbound : ∀ x, ⟪x, D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) (w : E) :
    ‖(T.symm : E →L[ℝ] E).adjoint (D w)‖ ≤
      Real.sqrt epsilon * Real.sqrt ⟪w, D w⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inner_primal_dual line 72
Source documentation
Primal-dual pairing is invariant under the frozen normalization.
```
theorem inner_primal_dual (T : E ≃L[ℝ] E) (x w : E) :
    ⟪T x, (T.symm : E →L[ℝ] E).adjoint w⟫_ℝ = ⟪x, w⟫_ℝ := by
…
```
theorem OAI.RegularPointCoordinates.abs_inner_le_frozen_primal_mul_dual line 77
theorem OAI.RegularPointCoordinates.frozen_positive_form_inner_abs_le line 84
Source documentation
Positive-form Cauchy--Schwarz has unchanged directional energies after the frozen normalization.
```
theorem frozen_positive_form_inner_abs_le (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) (x y : E) :
    |⟪T x, frozenConjugate T D (T y)⟫_ℝ| ≤
      Real.sqrt ⟪x, D x⟫_ℝ * Real.sqrt ⟪y, D y⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.frozenConjugate

theorem OAI.RegularPointCoordinates.frozen_positive_form_norm_le_primal line 93

Source documentation

The same small form has mixed operator norm at most epsilon, from the frozen primal norm to its dual norm.

theorem frozen_positive_form_norm_le_primal (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hbound : ∀ x, ⟪x, D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) (w : E) :
    ‖(T.symm : E →L[ℝ] E).adjoint (D w)‖ ≤ epsilon * ‖T w‖ := by
…

theorem OAI.RegularPointCoordinates.frozen_positive_form_mixed_opNorm_le line 102

theorem OAI.RegularPointCoordinates.frozen_positive_form_value_le line 113

Source documentation

A directional displacement-energy estimate gives the dual field-value bound used by each patch.

theorem frozen_positive_form_value_le (T : E ≃L[ℝ] E) {D : E →L[ℝ] E}
    (hD : D.IsPositive) {epsilon C r energy : ℝ}
    (hepsilon : 0 ≤ epsilon) (hC : 0 ≤ C) (hr : 0 ≤ r) (henergy : 0 ≤ energy)
    (hbound : ∀ x, ⟪x, D x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2)
    (w : E) (hw : ⟪w, D w⟫_ℝ ≤ C * r ^ 2 * energy) :
    ‖(T.symm : E →L[ℝ] E).adjoint (D w)‖ ≤
      Real.sqrt epsilon * Real.sqrt C * r * Real.sqrt energy := by
…

theorem OAI.RegularPointCoordinates.frozen_positive_patch_sum_norm_le line 130

Source documentation

Finite cutoff errors and field values may be estimated in the same dual norm while retaining each patch's directional energy.

theorem frozen_positive_patch_sum_norm_le {ι : Type*}
    (T : E ≃L[ℝ] E) (s : Finset ι) (D : ι → E →L[ℝ] E)
    (w : ι → E) (a : ι → ℝ) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hD : ∀ j ∈ s, (D j).IsPositive)
    (hbound : ∀ j ∈ s, ∀ x, ⟪x, D j x⟫_ℝ ≤ epsilon * ‖T x‖ ^ 2) :
    ‖(T.symm : E →L[ℝ] E).adjoint (∑ j ∈ s, a j • D j (w j))‖ ≤
      ∑ j ∈ s, |a j| * (Real.sqrt epsilon * Real.sqrt ⟪w j, D j (w j)⟫_ℝ) := by
…