EuclideanGreenIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact-test Green identity in Euclidean space

theorem OAI.RegularPointCoordinates.integral_second_directional_commute line 16

Source documentation

Two integrations by parts move a second directional derivative to its compactly supported test function.

theorem integral_second_directional_commute {n : ℕ} {f g : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (hgs : HasCompactSupport g)
    (v : Euclidean n) :
    (∫ x, f x*fderiv ℝ (fun y => fderiv ℝ g y v) x v) =
      ∫ x, fderiv ℝ (fun y => fderiv ℝ f y v) x v*g x := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.integral_directional_pairing line 49

Source documentation

A first-order gradient pairing against a compact test equals the negative second directional pairing.

theorem integral_directional_pairing {n : ℕ} {f g : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 1 g) (hgs : HasCompactSupport g)
    (v : Euclidean n) :
    (∫ x, fderiv ℝ f x v*fderiv ℝ g x v) =
      -∫ x, fderiv ℝ (fun y => fderiv ℝ f y v) x v*g x := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.laplacian_eq_sum_second_directional line 68

Source documentation

The coordinate trace of the actual second derivative.

theorem laplacian_eq_sum_second_directional {n : ℕ} {f : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) :
    Δ f = fun x => ∑ i : Fin n,
      fderiv ℝ (fun y => fderiv ℝ f y (EuclideanSpace.single i 1)) x (EuclideanSpace.single i 1) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.integral_laplacian_commute line 82

Source documentation

Green's identity with no boundary term for a compact test.

theorem integral_laplacian_commute {n : ℕ} {f g : Euclidean n → ℝ}
    (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (hgs : HasCompactSupport g) :
    (∫ x, f x*(Δ g) x) = ∫ x, (Δ f) x*g x := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean