ExactFormCoordinates.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.fluxCoordinates line 14
Source documentation
Coordinates in the positively oriented orthonormal frame already used by sphereFlux.
```
def fluxCoordinates (k : ℕ) :
    (Fin ((2*k+1)+1) → ℝ) ≃L[ℝ] ComplexEuclidean (k+1) :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
lemma OAI.Mahler.fluxCoordinates_basis line 19
lemma OAI.Mahler.fluxCoordinates_repr line 24
lemma OAI.Mahler.norm_fluxCoordinates_sq line 28

def OAI.Mahler.realFormCLM line 34

Source documentation

Real-part projection on continuous forms, as a continuous linear map.

def realFormCLM (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] (q : ℕ) :
    (E [⋀^Fin q]→L[ℝ] ℂ) →L[ℝ] (E [⋀^Fin q]→L[ℝ] ℝ) :=
…

lemma OAI.Mahler.realFormCLM_apply line 38

theorem OAI.Mahler.extDeriv_realForm line 44

Source documentation

Exterior differentiation commutes with taking the real part; C1 supplies only the first derivative used here.

theorem extDeriv_realForm {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {q : ℕ} {eta : E → E [⋀^Fin q]→L[ℝ] ℂ} {x : E}
    (h : DifferentiableAt ℝ eta x) :
    extDeriv (fun y => realFormCLM E q (eta y)) x =
      realFormCLM E (q+1) (extDeriv eta x) := by
…

Mentions: OAI.Mahler.realFormCLM

def OAI.Mahler.fluxPullback line 65

Source documentation

The actual real coordinate form, with the same ordered slots as eta.

def fluxPullback {k q : ℕ}
    (eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin q]→L[ℝ] ℂ)
    (x : Fin ((2*k+1)+1) → ℝ) :
    (Fin ((2*k+1)+1) → ℝ) [⋀^Fin q]→L[ℝ] ℝ :=
…

Mentions: OAI.Mahler.ComplexEuclidean

lemma OAI.Mahler.contDiffOn_fluxPullback line 72

theorem OAI.Mahler.extDeriv_fluxPullback line 83

Source documentation

Naturality for the actual fixed linear coordinates, requiring only a first derivative of eta. The coordinate map itself is smooth.

theorem extDeriv_fluxPullback {k q : ℕ}
    {eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin q]→L[ℝ] ℂ}
    {x : Fin ((2*k+1)+1) → ℝ} (h : DifferentiableAt ℝ eta (fluxCoordinates k x)) :
    extDeriv (fluxPullback eta) x = fluxPullback (extDeriv eta) x := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.fluxCoordinates, OAI.Mahler.fluxPullback