CapInverseBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.graphInverseMetric line 12
Source documentation
The literal inverse-Hessian norm of a restricted ambient affine covector.
```
def graphInverseMetric {n : ℕ} (u : Space n → ℝ)
    (a : Space n →L[ℝ] ℝ) (b d : ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.graphInverseMetric_nonneg line 18
lemma OAI.AffineBernstein.contDiffAt_graphInverseMetric line 26

theorem OAI.AffineBernstein.affineMaximal_graph_cap_inverse_bound line 46

Source documentation

The cap identity gives the genuine inverse-Hessian integral bound. The hypotheses are geometric support and scalar cutoff bounds, not a bound on the inverse Hessian. The right side is the area's actual integral, so the separate area-in-a-ball geometric theorem is not silently assumed.

theorem affineMaximal_graph_cap_inverse_bound {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (o : Space n) (c : ℝ) (a : Space n →L[ℝ] ℝ) (b d : ℝ)
    {ψ : ℝ → ℝ} (hψ : ContDiff ℝ ∞ ψ)
    {K Q : Set (Space n)} (hK : IsCompact K) (hKΩ : K ⊆ Ω)
    (hQ : MeasurableSet Q) (hQK : Q ⊆ K)
    (hs : ∀ x ∈ Ω, x ∉ K →
      ψ (graphAffineFunction u a b d x) = 0 ∧
      deriv ψ (graphAffineFunction u a b d x) = 0 ∧
      deriv (deriv ψ) (graphAffineFunction u a b d x) = 0)
    (hZ : ∀ x ∈ K, 0 ≤ radialSupport u o c x)
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.graphAffineFunction, OAI.AffineBernstein.radialSupport