CompactIntegration.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.integrable_of_support_subset_compact line 19

Source documentation

Integrability uses continuity only on a compact set containing the support.

theorem integrable_of_support_subset_compact {f : E → ℝ} {K : Set E}
    (hK : IsCompact K) (hs : Function.support f ⊆ K) (hf : ContinuousOn f K) :
    Integrable f μ :=
…

theorem OAI.AffineBernstein.integral_mul_fderiv_compact line 27

Source documentation

Compact support of the test function removes any global regularity requirement on the coefficient. This is the integration-by-parts form used on the original Ω.

theorem integral_mul_fderiv_compact (f g : E → ℝ) (v : E)
    (hf : ∀ x ∈ tsupport g, ContDiffAt ℝ 1 f x)
    (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) :
    (∫ x, f x * fderiv ℝ g x v ∂μ) =
      -(∫ x, fderiv ℝ f x v * g x ∂μ) := by
…

theorem OAI.AffineBernstein.integral_mul_second_fderiv_compact line 56

Source documentation

Two integrations by parts, without an artificial globally smooth coefficient.

theorem integral_mul_second_fderiv_compact (a η : E → ℝ) (v z : E)
    (ha : ∀ x ∈ tsupport η, ContDiffAt ℝ 2 a x)
    (hη : ContDiff ℝ 2 η) (hηc : HasCompactSupport η) :
    (∫ x, a x * fderiv ℝ (fun y => fderiv ℝ η y v) x z ∂μ) =
      ∫ x, fderiv ℝ (fun y => fderiv ℝ a y z) x v * η x ∂μ := by
…

theorem OAI.AffineBernstein.contDiff_dirDeriv line 72
Source documentation
Global smoothness of a fixed-direction derivative.
```
theorem contDiff_dirDeriv {f : E → ℝ} (hf : ContDiff ℝ ∞ f) (v : E) :
    ContDiff ℝ ∞ (dirDeriv v f) :=
…
```
Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.integral_double_contraction_compact line 77

Source documentation

The weak double-divergence formula with precisely a compactly supported test.

theorem integral_double_contraction_compact {ι : Type*} [Fintype ι]
    (a : ι → ι → E → ℝ) (e : ι → E) (η : E → ℝ)
    (ha : ∀ i j x, x ∈ tsupport η → ContDiffAt ℝ ∞ (a i j) x)
    (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η) :
    (∫ x, ∑ i, ∑ j, a i j x * dirDeriv (e i) (dirDeriv (e j) η) x ∂μ) =
      ∫ x, (∑ j, ∑ i, dirDeriv (e j) (dirDeriv (e i) (a i j)) x) * η x ∂μ := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.affineMaximal_weak_stationarity line 125

Source documentation

Graph-direction stationarity for the source's equation and actual coefficient. All regularity of u is needed only on the original open domain.

theorem affineMaximal_weak_stationarity {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) (hmax : AffineMaximalOn Ω u)
    (η : Space n → ℝ) (hη : ContDiff ℝ ∞ η) (hηc : HasCompactSupport η)
    (hηΩ : tsupport η ⊆ Ω) :
    (∫ x, ∑ i, ∑ j, affineWeight u x * cofactorHessian u x i j * hessian η x i j) = 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineWeight, OAI.AffineBernstein.cofactorHessian

def OAI.AffineBernstein.affineAreaDensity line 149
Source documentation
The density of affine area in the original graph coordinates.
```
def affineAreaDensity {n : ℕ} (u : Space n → ℝ) (x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.affineWeight_mul_det line 153
Source documentation
The variation coefficient has exactly the exponent in the manuscript.
```
theorem affineWeight_mul_det {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hpos : (hessian u x).PosDef) :
    affineWeight u x * (hessian u x).det = affineAreaDensity u x := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineWeight, OAI.AffineBernstein.affineAreaDensity
theorem OAI.AffineBernstein.affine_weight_cofactor_entry line 165
Source documentation
wU is not a surrogate for the affine-area coefficient.
```
theorem affine_weight_cofactor_entry {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hpos : (hessian u x).PosDef) (i j : Fin n) :
    affineWeight u x * cofactorHessian u x i j =
      affineAreaDensity u x * (hessian u x)⁻¹ i j := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineWeight, OAI.AffineBernstein.cofactorHessian, OAI.AffineBernstein.affineAreaDensity

theorem OAI.AffineBernstein.affineMaximal_area_stationarity line 173

Source documentation

The source's first-variation integral, over its original open domain.

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

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