SourceCoordinateExterior.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.extDeriv_sourceCoordinateForm line 13
theorem OAI.Mahler.MassHypotheses.coordinate_energy_extDeriv line 31
theorem OAI.Mahler.MassHypotheses.coordinate_log_extDeriv_nonneg line 41
Source documentation
The punctured Stokes integrand is nonnegative, using the nonnegative logarithmic complex Hessian in the positive frame.
```
theorem MassHypotheses.coordinate_log_extDeriv_nonneg (h : MassHypotheses (k+1) N m U f G)
    {x : Fin ((2*k+1)+1) → ℝ} (hx : sourceCoordinates k x ∈ U) (hne : x ≠ 0) :
    0 ≤ extDeriv (sourceCoordinateForm (sourceCoordinates k) (logTau f) k) x
      (MahlerStokes.coordinateBasis ((2*k+1)+1)) := by
…
```
Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.sourceCoordinates, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.logTau, OAI.MahlerStokes.coordinateBasis