OperatorQuadraticDerivative.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Operator derivatives from finitely many quadratic tests

Polarization uses only the coordinate vectors and their pairwise sums. This lets the scalar harmonic heat equations supply an operator equation, and lets finitely many annular error estimates control every direction.

def OAI.RegularPointCoordinates.operatorEntries line 25
def OAI.RegularPointCoordinates.matrixOperator line 28
theorem OAI.RegularPointCoordinates.matrixOperator_entries line 32

theorem OAI.RegularPointCoordinates.symmetric_entry_polarization line 48

Source documentation

The entry of a symmetric operator is obtained by real polarization.

theorem symmetric_entry_polarization (A : Euclidean n →L[ℝ] Euclidean n)
    (hA : A.IsSymmetric) (i j : Fin n) :
    A (EuclideanSpace.single j 1) i = (1 / 2 : ℝ) *
      (⟪EuclideanSpace.single i 1 + EuclideanSpace.single j 1,
          A (EuclideanSpace.single i 1 + EuclideanSpace.single j 1)⟫_ℝ -
       ⟪EuclideanSpace.single i 1, A (EuclideanSpace.single i 1)⟫_ℝ -
       ⟪EuclideanSpace.single j 1, A (EuclideanSpace.single j 1)⟫_ℝ) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

def OAI.RegularPointCoordinates.polarizedMatrix line 67
def OAI.RegularPointCoordinates.polarizedDerivative line 73
Source documentation
The operator formed by polarizing candidate quadratic derivatives.
```
def polarizedDerivative (d : Euclidean n → ℝ) : Euclidean n →L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.integrable_polarizedDerivative line 77

Source documentation

Integrability of the finite polarization follows from its scalar tests.

theorem integrable_polarizedDerivative {X : Type*} [MeasurableSpace X]
    (μ : MeasureTheory.Measure X) (d : X → Euclidean n → ℝ)
    (hs : ∀ i, MeasureTheory.Integrable (fun x => d x (EuclideanSpace.single i 1)) μ)
    (hp : ∀ i j, MeasureTheory.Integrable (fun x =>
      d x (EuclideanSpace.single i 1 + EuclideanSpace.single j 1)) μ) :
    MeasureTheory.Integrable (fun x => polarizedDerivative (d x)) μ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative

theorem OAI.RegularPointCoordinates.polarizedDerivative_isSymmetric line 95
Source documentation
The finite polarization is symmetric, even before a quadratic identity is known.
```
theorem polarizedDerivative_isSymmetric (d : Euclidean n → ℝ) :
    (polarizedDerivative d).IsSymmetric := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative
theorem OAI.RegularPointCoordinates.polarizedDerivative_add line 107
theorem OAI.RegularPointCoordinates.polarizedDerivative_sub line 116
theorem OAI.RegularPointCoordinates.polarizedDerivative_smul line 125
theorem OAI.RegularPointCoordinates.polarizedDerivative_quadratic_form line 135
Source documentation
Polarization recovers an existing symmetric operator exactly.
```
theorem polarizedDerivative_quadratic_form (A : Euclidean n →L[ℝ] Euclidean n)
    (hA : A.IsSymmetric) : polarizedDerivative (fun v => ⟪v, A v⟫_ℝ) = A := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative

theorem OAI.RegularPointCoordinates.polarizedDerivative_norm_le line 144

Source documentation

Only the coordinate vectors and their pairwise sums are needed for a uniform bound on the polarized operator.

theorem polarizedDerivative_norm_le (d : Euclidean n → ℝ) {ε : ℝ} (hε : 0 ≤ ε)
    (hsingle : ∀ i, |d (EuclideanSpace.single i 1)| ≤ ε)
    (hpair : ∀ i j, |d (EuclideanSpace.single i 1 + EuclideanSpace.single j 1)| ≤ ε) :
    ‖polarizedDerivative d‖ ≤ (n : ℝ) ^ 2 * (3 / 2 * ε) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative

theorem OAI.RegularPointCoordinates.hasDerivAt_operator_of_quadratic line 165
Source documentation
Finitely many differentiable quadratic tests determine the derivative of a symmetric operator-valued curve.
```
theorem hasDerivAt_operator_of_quadratic {Q : ℝ → (Euclidean n →L[ℝ] Euclidean n)}
    (hQ : ∀ t, (Q t).IsSymmetric) {t : ℝ} (d : Euclidean n → ℝ)
    (hd : ∀ v, HasDerivAt (fun s => ⟪v, Q s v⟫_ℝ) (d v) t) :
    HasDerivAt Q (polarizedDerivative d) t := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative
theorem OAI.RegularPointCoordinates.polarizedDerivative_quadratic line 183
Source documentation
The resulting operator derivative agrees with all quadratic tests, including directions that were not used in its finite construction.
```
theorem polarizedDerivative_quadratic {Q : ℝ → (Euclidean n →L[ℝ] Euclidean n)}
    (hQ : ∀ t, (Q t).IsSymmetric) {t : ℝ} (d : Euclidean n → ℝ)
    (hd : ∀ v, HasDerivAt (fun s => ⟪v, Q s v⟫_ℝ) (d v) t) (v : Euclidean n) :
    ⟪v, polarizedDerivative d v⟫_ℝ = d v := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative