DeterminantVariation.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.hasDerivAt_det_line line 18

Source documentation

Jacobi's formula without assuming invertibility of the varied matrix.

theorem hasDerivAt_det_line (A B : Matrix ι ι ℝ) :
    HasDerivAt (fun t : ℝ => (A + t • B).det)
      (∑ i, ∑ j, A.adjugate j i * B i j) 0 := by
…

theorem OAI.AffineBernstein.hasDerivAt_affineArea_matrix line 41

Source documentation

Pointwise first variation of the actual affine-area density.

theorem hasDerivAt_affineArea_matrix (A B : Matrix ι ι ℝ) (hA : A.PosDef) (δ : ℝ) :
    HasDerivAt (fun t : ℝ => Real.rpow (A + t • B).det δ)
      (δ * Real.rpow A.det (δ - 1) * (∑ i, ∑ j, A.adjugate j i * B i j)) 0 := by
…

theorem OAI.AffineBernstein.contDiff_of_contDiffAt_tsupport line 58
Source documentation
Away from topological support the test is locally zero, so no extension of a smooth coefficient across the original boundary is necessary.
```
theorem contDiff_of_contDiffAt_tsupport {f : E → ℝ} {k : ℕ∞ω}
    (hf : ∀ x ∈ tsupport f, ContDiffAt ℝ k f x) : ContDiff ℝ k f := by
…
```
theorem OAI.AffineBernstein.dirDeriv_eq_second line 68
Source documentation
Commuting fixed-direction differentiation with evaluation of a derivative.
```
theorem dirDeriv_eq_second {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ ∞ f x) (v z : E) :
    dirDeriv v (dirDeriv z f) x = fderiv ℝ (fderiv ℝ f) x v z := by
…
```
Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.dirDeriv_comm line 77

Source documentation

Symmetry of the second derivative in fixed directions.

theorem dirDeriv_comm {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ ∞ f x) (v z : E) :
    dirDeriv v (dirDeriv z f) x = dirDeriv z (dirDeriv v f) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

def OAI.AffineBernstein.radialSupport line 83
Source documentation
The support-plane height ν(o-X) in original graph coordinates.
```
def radialSupport (u : E → ℝ) (o : E) (c : ℝ) (x : E) : ℝ :=
…
```
theorem OAI.AffineBernstein.contDiffAt_radialSupport line 87
Source documentation
Smoothness holds only locally; the eventual zero argument handles tests.
```
theorem contDiffAt_radialSupport {u : E → ℝ} {x : E}
    (hu : ContDiffAt ℝ ∞ u x) (o : E) (c : ℝ) :
    ContDiffAt ℝ ∞ (radialSupport u o c) x :=
…
```
Mentions: OAI.AffineBernstein.radialSupport

theorem OAI.AffineBernstein.dirDeriv_radialGradient line 94

Source documentation

The derivative of the radial gradient, including its moving vector argument.

theorem dirDeriv_radialGradient {u : E → ℝ} {x : E}
    (hu : ContDiffAt ℝ ∞ u x) (o v : E) :
    dirDeriv v (fun y => fderiv ℝ u y (y - o)) x =
      dirDeriv (x - o) (dirDeriv v u) x + dirDeriv v u x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.dirDeriv_radialSupport line 109
Source documentation
The cancellation D Z = H(x-o) with no coordinate or global extension assumption.
```
theorem dirDeriv_radialSupport {u : E → ℝ} {x : E}
    (hu : ContDiffAt ℝ ∞ u x) (o : E) (c : ℝ) (v : E) :
    dirDeriv v (radialSupport u o c) x = dirDeriv (x - o) (dirDeriv v u) x := by
…
```
Mentions: OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.radialSupport

theorem OAI.AffineBernstein.second_dirDeriv_radialSupport line 128

Source documentation

The exact second derivative of the support-plane height.

theorem second_dirDeriv_radialSupport {Ω : Set E} (hΩ : IsOpen Ω)
    {u : E → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) {x : E} (hx : x ∈ Ω)
    (o : E) (c : ℝ) (v z : E) :
    dirDeriv z (dirDeriv v (radialSupport u o c)) x =
      dirDeriv z (dirDeriv v u) x +
        dirDeriv (x - o) (dirDeriv z (dirDeriv v u)) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.radialSupport

theorem OAI.AffineBernstein.hessian_radialSupport line 146

Source documentation

The coordinate version used in the trace of the cap test.

theorem hessian_radialSupport {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) {x : Space n} (hx : x ∈ Ω)
    (o : Space n) (c : ℝ) (i j : Fin n) :
    hessian (radialSupport u o c) x i j = hessian u x i j +
      dirDeriv (x - o) (fun y => hessian u y i j) x :=
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.radialSupport, OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.dirDeriv_det line 154

Source documentation

Jacobi's formula in arbitrary fixed directions, for the actual entries.

theorem dirDeriv_det {E ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [Fintype ι] [DecidableEq ι] (A : E → Matrix ι ι ℝ) {x : E}
    (hA : ∀ i j, DifferentiableAt ℝ (fun y => A y i j) x) (v : E) :
    dirDeriv v (fun y => (A y).det) x =
      ∑ i, ∑ j, (A x).adjugate j i * dirDeriv v (fun y => A y i j) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.contDiffAt_affineAreaDensity line 176
Source documentation
Smoothness of the area density on the original domain.
```
theorem contDiffAt_affineAreaDensity {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (hpos : (hessian u x).PosDef) :
    ContDiffAt ℝ ∞ (affineAreaDensity u) x :=
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.dirDeriv_affineAreaDensity line 182

Source documentation

The exact differential of the affine area coefficient.

theorem dirDeriv_affineAreaDensity {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (hpos : (hessian u x).PosDef) (v : Space n) :
    dirDeriv v (affineAreaDensity u) x =
      (1 / ((n : ℝ) + 2)) * affineAreaDensity u x *
        (∑ i, ∑ j, (hessian u x)⁻¹ i j * dirDeriv v (fun y => hessian u y i j) x) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.trace_inverse_mul_self line 216

Source documentation

Trace of the identity, in the entry convention used in the manuscript.

theorem trace_inverse_mul_self {n : ℕ} {H : Matrix (Fin n) (Fin n) ℝ}
    (hH : H.PosDef) : (∑ i, ∑ j, H⁻¹ i j * H i j) = (n : ℝ) := by
…

theorem OAI.AffineBernstein.weighted_trace_radialSupport line 231

Source documentation

Weighted radial trace, avoiding a logarithm at points outside the domain.

theorem weighted_trace_radialSupport {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    {x : Space n} (hx : x ∈ Ω) (hpos : (hessian u x).PosDef)
    (o : Space n) (c : ℝ) :
    affineAreaDensity u x *
      (∑ i, ∑ j, (hessian u x)⁻¹ i j * hessian (radialSupport u o c) x i j) =
        n * affineAreaDensity u x + ((n : ℝ) + 2) * dirDeriv (x - o) (affineAreaDensity u) x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineAreaDensity, OAI.AffineBernstein.radialSupport, OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.sum_coordinateVector line 245
Source documentation
Expansion in the frozen Euclidean coordinate vectors.
```
theorem sum_coordinateVector {n : ℕ} (v : Space n) :
    (∑ i, (v i) • coordinateVector n i) = v := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.coordinateVector
theorem OAI.AffineBernstein.clm_coordinate_sum line 251
Source documentation
Linear functionals are recovered exactly by coordinates.
```
theorem clm_coordinate_sum {n : ℕ} (L : Space n →L[ℝ] ℝ) (v : Space n) :
    L v = ∑ i, v i * L (coordinateVector n i) := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.coordinateVector
theorem OAI.AffineBernstein.dirDeriv_coordinate_sum line 257
Source documentation
The radial vector derivative is the sum of its coordinate derivatives.
```
theorem dirDeriv_coordinate_sum {n : ℕ} (f : Space n → ℝ) (x v : Space n) :
    dirDeriv v f x = ∑ i, v i * dirDeriv (coordinateVector n i) f x :=
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector

theorem OAI.AffineBernstein.second_dirDeriv_mul line 262

Source documentation

A second derivative product rule on the actual open domain.

theorem second_dirDeriv_mul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {Ω : Set E} (hΩ : IsOpen Ω) {f g : E → ℝ}
    (hf : ContDiffOn ℝ ∞ f Ω) (hg : ContDiffOn ℝ ∞ g Ω)
    {x : E} (hx : x ∈ Ω) (v z : E) :
    dirDeriv z (dirDeriv v (fun y => f y * g y)) x =
      dirDeriv z (dirDeriv v f) x * g x + dirDeriv v f x * dirDeriv z g x +
      dirDeriv z f x * dirDeriv v g x + f x * dirDeriv z (dirDeriv v g) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.dirDeriv_comp_scalar line 291

Source documentation

Scalar composition by its actual one-dimensional derivative.

theorem dirDeriv_comp_scalar {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {q : E → ℝ} {ψ : ℝ → ℝ} {x : E} (hq : DifferentiableAt ℝ q x)
    (hψ : DifferentiableAt ℝ ψ (q x)) (v : E) :
    dirDeriv v (fun y => ψ (q y)) x = deriv ψ (q x) * dirDeriv v q x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.second_dirDeriv_comp_scalar line 301

Source documentation

The second chain rule used by a cap test.

theorem second_dirDeriv_comp_scalar {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {Ω : Set E} (hΩ : IsOpen Ω) {q : E → ℝ} {ψ : ℝ → ℝ}
    (hq : ContDiffOn ℝ ∞ q Ω) (hψ : ContDiff ℝ ∞ ψ)
    {x : E} (hx : x ∈ Ω) (v z : E) :
    dirDeriv z (dirDeriv v (fun y => ψ (q y))) x =
      deriv (deriv ψ) (q x) * dirDeriv z q x * dirDeriv v q x +
      deriv ψ (q x) * dirDeriv z (dirDeriv v q) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

def OAI.AffineBernstein.graphAffineFunction line 326
Source documentation
Restriction of an arbitrary ambient affine function to the original graph.
```
def graphAffineFunction {n : ℕ} (u : Space n → ℝ) (a : Space n →L[ℝ] ℝ)
    (b d : ℝ) (x : Space n) : ℝ := a x + b * u x + d
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.contDiffAt_graphAffineFunction line 329
theorem OAI.AffineBernstein.dirDeriv_graphAffineFunction line 334
theorem OAI.AffineBernstein.hessian_graphAffineFunction line 342

theorem OAI.AffineBernstein.matrix_pair_eq_dot line 359

Source documentation

Coordinate pairing equals the ordinary matrix-vector contraction.

theorem matrix_pair_eq_dot {ι : Type*} [Fintype ι]
    (A : Matrix ι ι ℝ) (p q : ι → ℝ) :
    (∑ i, ∑ j, A i j * p i * q j) = p ⬝ᵥ (A.mulVec q) := by
…

theorem OAI.AffineBernstein.matrix_pair_symm line 370

Source documentation

Symmetry of the covector contraction, with the literal matrix coefficients.

theorem matrix_pair_symm {ι : Type*} [Fintype ι]
    {A : Matrix ι ι ℝ} (hA : A.IsSymm) (p q : ι → ℝ) :
    (∑ i, ∑ j, A i j * p i * q j) = ∑ i, ∑ j, A i j * q i * p j := by
…

theorem OAI.AffineBernstein.inverse_radial_contraction line 382

Source documentation

Exact inverse contraction for a radial vector and a covector.

theorem inverse_radial_contraction {ι : Type*} [Fintype ι] [DecidableEq ι]
    {H : Matrix ι ι ℝ} (hH : H.PosDef) (v p : ι → ℝ) :
    (∑ i, ∑ j, H⁻¹ i j * (∑ k, v k * H k i) * p j) = ∑ i, v i * p i := by
…

theorem OAI.AffineBernstein.inverseHessian_radialSupport line 392

Source documentation

The radial support gradient cancels exactly against the inverse Hessian.

theorem inverseHessian_radialSupport {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) (hpos : (hessian u x).PosDef)
    (o : Space n) (c : ℝ) (q : Space n → ℝ) :
    (∑ i, ∑ j, (hessian u x)⁻¹ i j *
      dirDeriv (coordinateVector n i) (radialSupport u o c) x *
      dirDeriv (coordinateVector n j) q x) = dirDeriv (x - o) q x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector, OAI.AffineBernstein.radialSupport

theorem OAI.AffineBernstein.hessian_product_trace line 407

Source documentation

Product trace in coordinates.

theorem hessian_product_trace {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {f g : Space n → ℝ} (hf : ContDiffOn ℝ ∞ f Ω) (hg : ContDiffOn ℝ ∞ g Ω)
    {x : Space n} (hx : x ∈ Ω) {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.IsSymm) :
    (∑ i, ∑ j, A i j * hessian (fun y => f y * g y) x i j) =
      g x * (∑ i, ∑ j, A i j * hessian f x i j) +
      f x * (∑ i, ∑ j, A i j * hessian g x i j) +
      2 * (∑ i, ∑ j, A i j * dirDeriv (coordinateVector n i) f x *
        dirDeriv (coordinateVector n j) g x) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector

theorem OAI.AffineBernstein.hessian_composition_trace line 456

Source documentation

Chain trace in coordinates.

theorem hessian_composition_trace {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {q : Space n → ℝ} {ψ : ℝ → ℝ}
    (hq : ContDiffOn ℝ ∞ q Ω) (hψ : ContDiff ℝ ∞ ψ)
    {x : Space n} (hx : x ∈ Ω) (A : Matrix (Fin n) (Fin n) ℝ) :
    (∑ i, ∑ j, A i j * hessian (fun y => ψ (q y)) x i j) =
      deriv (deriv ψ) (q x) * (∑ i, ∑ j, A i j *
        dirDeriv (coordinateVector n i) q x * dirDeriv (coordinateVector n j) q x) +
      deriv ψ (q x) * (∑ i, ∑ j, A i j * hessian q x i j) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector

theorem OAI.AffineBernstein.inverseHessian_isSymm line 473
Source documentation
Positivity fixes the inverse-Hessian symmetry employed in a cap test.
```
theorem inverseHessian_isSymm {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hpos : (hessian u x).PosDef) : ((hessian u x)⁻¹).IsSymm :=
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.weighted_trace_capTest line 478

Source documentation

Pointwise first-variation integrand of the source cap test.

theorem weighted_trace_capTest {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) {x : Space n} (hx : x ∈ Ω)
    (hpos : (hessian u x).PosDef) (o : Space n) (c : ℝ)
    (a : Space n →L[ℝ] ℝ) (b d : ℝ) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ ∞ ψ) :
    let q := graphAffineFunction u a b d
…

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

theorem OAI.AffineBernstein.cap_affine_cancellation line 537

Source documentation

Cancellation of the affine coefficients in the first variation.

theorem cap_affine_cancellation {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : DifferentiableAt ℝ u x) (o : Space n) (c : ℝ)
    (a : Space n →L[ℝ] ℝ) (b d : ℝ) :
    radialSupport u o c x * b - dirDeriv (x - o) (graphAffineFunction u a b d) x =
      (a o + b * c + d) - graphAffineFunction u a b d x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.radialSupport, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.graphAffineFunction

def OAI.AffineBernstein.coordinateProjection line 547
Source documentation
The actual coordinate functional through the Euclidean-space equivalence.
```
def coordinateProjection (n : ℕ) (i : Fin n) : Space n →L[ℝ] ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.coordinateProjection_apply line 550

theorem OAI.AffineBernstein.contDiff_mul_at_tsupport line 554

Source documentation

A smooth compact test makes a merely locally smooth coefficient globally smooth.

theorem contDiff_mul_at_tsupport {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f g : E → ℝ} {k : ℕ∞ω} (hg : ContDiff ℝ k g)
    (hf : ∀ x ∈ tsupport g, ContDiffAt ℝ k f x) :
    ContDiff ℝ k (fun x => f x * g x) := by
…

theorem OAI.AffineBernstein.integral_dirDeriv_compact line 563

Source documentation

Integral of a derivative of a smooth compactly supported scalar field.

theorem integral_dirDeriv_compact {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {μ : Measure E} [μ.IsAddHaarMeasure]
    (f : E → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) (v : E) :
    (∫ x, dirDeriv v f x ∂μ) = 0 := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.integral_radial_divergence_compact line 575

Source documentation

Radial integration by parts with a compact test and no global extension of f. This formulation gives integrability as well as the identity.

theorem integral_radial_divergence_compact {n : ℕ}
    {μ : Measure (Space n)} [μ.IsAddHaarMeasure]
    (f σ : Space n → ℝ) (o : Space n)
    (hσ : ContDiff ℝ ∞ σ) (hσc : HasCompactSupport σ)
    (hf : ∀ x ∈ tsupport σ, ContDiffAt ℝ ∞ f x) :
    let D := fun x => dirDeriv (x - o) f x * σ x +
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.contDiff_indicator_of_compact line 654

Source documentation

Zero-extension of a compactly supported local test is genuinely smooth on the ambient coordinate space; no extension theorem for the graph is needed.

theorem contDiff_indicator_of_compact {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {Ω K : Set E} (hΩ : IsOpen Ω) (hK : IsCompact K)
    (hKΩ : K ⊆ Ω) {f : E → ℝ} {k : ℕ∞ω} (hf : ContDiffOn ℝ k f Ω)
    (hz : ∀ x ∈ Ω, x ∉ K → f x = 0) :
    ContDiff ℝ k (Ω.indicator f) ∧ HasCompactSupport (Ω.indicator f) ∧
      tsupport (Ω.indicator f) ⊆ K := by
…

theorem OAI.AffineBernstein.hessian_eq_of_eventuallyEq line 677
Source documentation
Hessians depend only on the germ of a function, also with the total derivative convention at points outside the domain.
```
theorem hessian_eq_of_eventuallyEq {n : ℕ} {f g : Space n → ℝ} {x : Space n}
    (h : f =ᶠ[nhds x] g) : hessian f x = hessian g x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

theorem OAI.AffineBernstein.integrableOn_area_variation line 686

Source documentation

The actual first-variation density is integrable for a compact local test.

theorem integrableOn_area_variation {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef)
    (η : Space n → ℝ) (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η)
    (hηΩ : tsupport η ⊆ Ω) :
    IntegrableOn (fun x => affineAreaDensity u x *
      (∑ i, ∑ j, (hessian u x)⁻¹ i j * hessian η x i j)) Ω := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.affineMaximal_graph_cap_identity line 719

Source documentation

The cap identity in the original graph coordinates (source area.tex, Lemma Cap identity). The source assumes compact support of all three displayed scalar compositions; this proof in fact only needs the first support condition. The measure here is precisely affine area density times Lebesgue measure.

theorem affineMaximal_graph_cap_identity {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) (hmax : AffineMaximalOn Ω u)
    (o : Space n) (c : ℝ) (a : Space n →L[ℝ] ℝ) (b d : ℝ)
    {ψ : ℝ → ℝ} (hψ : ContDiff ℝ ∞ ψ)
    {K : Set (Space n)} (hK : IsCompact K) (hKΩ : K ⊆ Ω)
    (hsupport : ∀ x ∈ Ω, x ∉ K → ψ (graphAffineFunction u a b d x) = 0) :
    (∫ x in Ω, affineAreaDensity u x *
      (radialSupport u o c x *
        (∑ i, ∑ j, (hessian u x)⁻¹ i j *
          dirDeriv (coordinateVector n i) (graphAffineFunction u a b d) x *
          dirDeriv (coordinateVector n j) (graphAffineFunction u a b d) x) *
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.graphAffineFunction, OAI.AffineBernstein.affineAreaDensity, OAI.AffineBernstein.radialSupport, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector