NormSquareForm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.normEnergy line 11
lemma OAI.Mahler.normEnergy_contDiff line 13
lemma OAI.Mahler.dc_normEnergy line 17
Source documentation
The actual d^c of the Euclidean squared norm.
```
lemma dc_normEnergy {n : ℕ} (x v : ComplexEuclidean n) :
    dc (normEnergy n) x v = (-1 / 2 : ℂ) * (inner ℝ x (I • v) : ℂ) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.dc, OAI.Mahler.normEnergy
lemma OAI.Mahler.real_inner_complexStructure_swap line 25
theorem OAI.Mahler.extDeriv_dc_normEnergy line 35
Source documentation
The exterior normalization dd^c |z|^2 is the standard symplectic two-form, with positive dx_k wedge dy_k orientation.
```
theorem extDeriv_dc_normEnergy {n : ℕ} (x v w : ComplexEuclidean n) :
    extDeriv (oneForm (dcLinear (normEnergy n))) x ![v, w] =
      ((∑ j : Fin n, ((v j).re * (w j).im - (v j).im * (w j).re) : ℝ) : ℂ) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.normEnergy