JacobianSquareRoot.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.JacobianSquareRoot.contDiff_matrix_det line 15

Source documentation

The determinant is a smooth polynomial in the matrix entries.

theorem contDiff_matrix_det {ι : Type uIndex} [Fintype ι] [DecidableEq ι]
    (n : WithTop ENat) : ContDiff ℝ n (Matrix.det : Matrix ι ι ℝ → ℝ) := by
…

theorem OAI.Problem356.JacobianSquareRoot.contDiff_clm_det line 28

Source documentation

The determinant is smooth on continuous linear endomorphisms in finite dimension.

theorem contDiff_clm_det {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (n : WithTop ENat) :
    ContDiff ℝ n (fun A : E →L[ℝ] E => A.det) := by
…

theorem OAI.Problem356.JacobianSquareRoot.contDiffOn_sqrt_abs_det line 40

Source documentation

Nonzero determinants yield smooth absolute-Jacobian square roots.

theorem contDiffOn_sqrt_abs_det
    {D : Type uD} {E : Type uE} [NormedAddCommGroup D] [NormedSpace ℝ D]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {n : WithTop ENat} {U : Set D} {A : D → E →L[ℝ] E}
    (hA : ContDiffOn ℝ n A U) (hdet : ∀ x ∈ U, (A x).det ≠ 0) :
    ContDiffOn ℝ n (fun x => Real.sqrt |(A x).det|) U := by
…

theorem OAI.Problem356.JacobianSquareRoot.det_ne_zero_of_isInvertible line 53
Source documentation
Invertibility of an endomorphism implies its Jacobian determinant is nonzero.
```
theorem det_ne_zero_of_isInvertible
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {A : E →L[ℝ] E} (hA : A.IsInvertible) : A.det ≠ 0 := by
…
```

theorem OAI.Problem356.JacobianSquareRoot.contDiffOn_sqrt_abs_det_fderiv line 60

Source documentation

Smoothness of the square root of the absolute derivative determinant on an open set.

theorem contDiffOn_sqrt_abs_det_fderiv
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {U : Set E} {F : E → E} (hU : IsOpen U)
    (hF : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) F U)
    (hdet : ∀ x ∈ U, (fderiv ℝ F x).det ≠ 0) :
    ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
      (fun x => Real.sqrt |(fderiv ℝ F x).det|) U := by
…

theorem OAI.Problem356.JacobianSquareRoot.contDiffOn_transportedAmplitude line 72

Source documentation

Multiplication by the composed source amplitude gives the local transported amplitude.

theorem contDiffOn_transportedAmplitude
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {U : Set E} {F : E → E} {g : E → ℝ} (hU : IsOpen U)
    (hF : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) F U)
    (hg : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g)
    (hdet : ∀ x ∈ U, (fderiv ℝ F x).det ≠ 0) :
    ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
      (fun x => g (F x) * Real.sqrt |(fderiv ℝ F x).det|) U :=
…

theorem OAI.Problem356.JacobianSquareRoot.det_fderiv_ne_zero_of_eventual_leftInverse line 83

Source documentation

An eventually defined differentiable left inverse forces a nonzero derivative determinant.

theorem det_fderiv_ne_zero_of_eventual_leftInverse
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {F G : E → E} {x : E} (hF : DifferentiableAt ℝ F x)
    (hG : DifferentiableAt ℝ G (F x))
    (hGF : ∀ᶠ y in nhds x, G (F y) = y) : (fderiv ℝ F x).det ≠ 0 := by
…

theorem OAI.Problem356.JacobianSquareRoot.det_fderiv_symm_ne_zero line 101

Source documentation

Both smooth directions of an open partial homeomorphism have nonvanishing inverse Jacobian.

theorem det_fderiv_symm_ne_zero
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e e.source)
    (he' : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e.symm e.target)
    {y : E} (hy : y ∈ e.target) : (fderiv ℝ e.symm y).det ≠ 0 := by
…

theorem OAI.Problem356.JacobianSquareRoot.contDiffOn_sqrt_abs_det_fderiv_symm line 113

Source documentation

Smooth inverse-Jacobian factor for a smooth open partial diffeomorphism.

theorem contDiffOn_sqrt_abs_det_fderiv_symm
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e e.source)
    (he' : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e.symm e.target) :
    ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
      (fun y => Real.sqrt |(fderiv ℝ e.symm y).det|) e.target :=
…

theorem OAI.Problem356.JacobianSquareRoot.contDiffOn_transportedAmplitude_symm line 124

Source documentation

Local transported amplitudes are smooth, with no separate Jacobian hypothesis.

theorem contDiffOn_transportedAmplitude_symm
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e e.source)
    (he' : ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat) e.symm e.target)
    {g : E → ℝ} (hg : ContDiff ℝ (↑(⊤ : ENat) : WithTop ENat) g) :
    ContDiffOn ℝ (↑(⊤ : ENat) : WithTop ENat)
      (fun y => g (e.symm y) * Real.sqrt |(fderiv ℝ e.symm y).det|) e.target :=
…

theorem OAI.Problem356.JacobianSquareRoot.transportedAmplitude_sq line 135

Source documentation

The transported amplitude squares to the Jacobian-weighted source density.

theorem transportedAmplitude_sq
    {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (F : E → E) (g : E → ℝ) (y : E) :
    (g (F y) * Real.sqrt |(fderiv ℝ F y).det|) ^ 2 =
      |(fderiv ℝ F y).det| * (g (F y)) ^ 2 := by
…