WeightedDivergence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.dirDeriv line 16
Source documentation
A fixed-direction derivative, used only as notation for the actual Fréchet derivative.
```
def dirDeriv (v : E) (f : E → ℝ) : E → ℝ := fun x => fderiv ℝ f x v
```
theorem OAI.AffineBernstein.contDiffAt_dirDeriv line 18
theorem OAI.AffineBernstein.dirDeriv_mul line 22
theorem OAI.AffineBernstein.dirDeriv_sum line 28

theorem OAI.AffineBernstein.double_divergence_weighted line 35

Source documentation

The differential part of the double integration by parts. Both zero cofactor divergences are used; they will be supplied by the proved Piola identity.

theorem double_divergence_weighted {Ω : Set E} (hΩ : IsOpen Ω)
    (U : E → ι → ι → ℝ) (w : E → ℝ) (e : ι → E)
    (hU : ∀ x ∈ Ω, ∀ i j, ContDiffAt ℝ ∞ (fun y => U y i j) x)
    (hw : ∀ x ∈ Ω, ContDiffAt ℝ ∞ w x)
    (hrow : ∀ x ∈ Ω, ∀ i, (∑ j, dirDeriv (e j) (fun y => U y i j) x) = 0)
    (hcol : ∀ x ∈ Ω, ∀ j, (∑ i, dirDeriv (e i) (fun y => U y i j) x) = 0)
    {x : E} (hx : x ∈ Ω) :
    (∑ j, ∑ i, dirDeriv (e j) (dirDeriv (e i) (fun y => w y * U y i j)) x) =
      ∑ j, ∑ i, U x i j * dirDeriv (e j) (dirDeriv (e i) w) x := by
…

Mentions: OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.affine_operator_eq_double_divergence line 94

Source documentation

The exact maximal-graph operator is the double divergence of its variational coefficient.

theorem affine_operator_eq_double_divergence {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hpos : ∀ y ∈ Ω, (hessian u y).PosDef) {x : Space n} (hx : x ∈ Ω) :
    (∑ j, ∑ i, dirDeriv (coordinateVector n j) (dirDeriv (coordinateVector n i)
      (fun y => affineWeight u y * cofactorHessian u y i j)) x) =
      ∑ i, ∑ j, cofactorHessian u x i j * hessian (affineWeight u) x i j := by
…

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