OrientedChartIntegral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.jacobianOrientation line 14
Source documentation
Orientation of a real Jacobian. Its value at zero is immaterial for change of variables; genuine local diffeomorphisms have nonzero Jacobian.
```
def jacobianOrientation (a : ℝ) : ℝ := if 0 ≤ a then 1 else -1
```
lemma OAI.MahlerStokes.jacobianOrientation_mul line 16

theorem OAI.MahlerStokes.topForm_apply_linear line 24

Source documentation

A top alternating form transforms by the determinant in the ordered standard coordinate basis.

theorem topForm_apply_linear {d : ℕ}
    (A : (Fin d → ℝ) [⋀^Fin d]→L[ℝ] ℝ) (L : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ)) :
    A (fun i => L (coordinateBasis d i)) = L.det * A (coordinateBasis d) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis

theorem OAI.MahlerStokes.integral_image_topForm line 43

Source documentation

Actual Lebesgue change of variables for an oriented top form. The orientation factor converts the signed determinant to the positive Jacobian.

theorem integral_image_topForm {d : ℕ} {s : Set (Fin d → ℝ)}
    (φ : (Fin d → ℝ) → (Fin d → ℝ))
    (A : (Fin d → ℝ) → (Fin d → ℝ) [⋀^Fin d]→L[ℝ] ℝ)
    (hs : MeasurableSet s) (hφ : ∀ x ∈ s, DifferentiableAt ℝ φ x) (hinj : InjOn φ s) :
    (∫ x in φ '' s, A x (coordinateBasis d)) =
      ∫ y in s, jacobianOrientation (fderiv ℝ φ y).det *
        A (φ y) (fun i => fderiv ℝ φ y (coordinateBasis d i)) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis, OAI.MahlerStokes.jacobianOrientation

theorem OAI.MahlerStokes.integral_image_extDeriv line 59

Source documentation

The actual exterior derivative on a C2 coordinate chart, with the Jacobian orientation made explicit in the volume integral.

theorem integral_image_extDeriv {n : ℕ} {s : Set (Fin (n+1) → ℝ)}
    (φ : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ))
    (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
    (hs : MeasurableSet s) (hφ : ∀ x ∈ s, ContDiffAt ℝ 2 φ x)
    (hinj : InjOn φ s) (hω : ∀ x ∈ s, DifferentiableAt ℝ ω (φ x)) :
    (∫ x in φ '' s, extDeriv ω x (coordinateBasis (n+1))) =
      ∫ y in s, jacobianOrientation (fderiv ℝ φ y).det *
        extDeriv (pullbackForm φ ω) y (coordinateBasis (n+1)) := by
…

Mentions: OAI.MahlerStokes.coordinateBasis, OAI.MahlerStokes.jacobianOrientation, OAI.MahlerStokes.pullbackForm

theorem OAI.MahlerStokes.jacobianOrientation_eventuallyEq line 77

Source documentation

At a nonzero Jacobian, orientation is locally constant.

theorem jacobianOrientation_eventuallyEq {E : Type*} [TopologicalSpace E]
    {f : E → ℝ} {x : E} (hf : ContinuousAt f x) (hx : f x ≠ 0) :
    (fun y => jacobianOrientation (f y)) =ᶠ[𝓝 x] (fun _ => jacobianOrientation (f x)) := by
…

Mentions: OAI.MahlerStokes.jacobianOrientation