DirectionalGradientBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From component gradient bounds to every constant direction

theorem OAI.RegularPointCoordinates.gamma_column_le_of_diagonal_bounds line 20

Source documentation

A finite family with uniformly bounded squared gradients gives the corresponding bound on every linear combination.

theorem gamma_column_le_of_diagonal_bounds {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
    (S : Set X) (B : ℝ)
    (hb : ∀ i, ∀ᵐ x ∂μ.restrict S, localGamma μ hQ (u i) (u i) x ≤ B ^ 2)
    (v : Euclidean n) :
    ∀ᵐ x ∂μ.restrict S,
      localGamma μ hQ (sobolevColumnMap μ hQ u v) (sobolevColumnMap μ hQ u v) x ≤
        ((n : ℝ) * B) ^ 2 * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.FirstOrderSplittingOn.directional_gradient line 65
Source documentation
The first-order splitting definition controls the gradient of every constant direction, not merely the coordinate columns.
```
theorem FirstOrderSplittingOn.directional_gradient {n : ℕ} {p : X} {r ε : ℝ}
    {u : Fin n → SobolevSpace μ hQ} {w : X → Euclidean n}
    (h : FirstOrderSplittingOn μ hQ p r ε u w) (v : Euclidean n) :
    ∀ᵐ x ∂μ.restrict (Metric.ball p r),
      localGamma μ hQ (sobolevColumnMap μ hQ u v) (sobolevColumnMap μ hQ u v) x ≤
        ((n : ℝ) * (1 + ε)) ^ 2 * ‖v‖ ^ 2 :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevColumnMap