ExteriorFlux.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.complexStructure line 16
Source documentation
Multiplication by i as a real continuous linear map.
```
noncomputable def complexStructure : E →L[ℝ] E :=
…
```
lemma OAI.Mahler.complexStructure_apply line 19
def OAI.Mahler.dcLinear line 22
Source documentation
The operator d^c, bundled as a real continuous linear one-form.
```
noncomputable def dcLinear (u : E → ℂ) (x : E) : E →L[ℝ] ℂ :=
…
```
lemma OAI.Mahler.dcLinear_apply line 25
def OAI.Mahler.oneForm line 30
Source documentation
A continuous linear one-form regarded as a continuous alternating one-form.
```
noncomputable def oneForm (a : E → E →L[ℝ] ℂ) (x : E) : E [⋀^Fin 1]→L[ℝ] ℂ :=
…
```
lemma OAI.Mahler.oneForm_apply line 34
lemma OAI.Mahler.differentiableAt_oneForm line 38

lemma OAI.Mahler.extDeriv_oneForm line 43

Source documentation

Exterior differentiation uses the usual unnormalized alternating sum.

lemma extDeriv_oneForm {a : E → E →L[ℝ] ℂ} {x : E}
    (ha : DifferentiableAt ℝ a x) (v w : E) :
    extDeriv (oneForm a) x ![v, w] =
      fderiv ℝ (fun y => a y w) x v - fderiv ℝ (fun y => a y v) x w := by
…

Mentions: OAI.Mahler.oneForm

lemma OAI.Mahler.hasDerivAt_circle_smul line 50
lemma OAI.Mahler.hasDerivAt_circle_form line 54
lemma OAI.Mahler.fderiv_circle_invariant line 69
lemma OAI.Mahler.fderiv_circle_contraction line 80
lemma OAI.Mahler.fderiv_form_apply line 91

theorem OAI.Mahler.extDeriv_circle_horizontal line 100

Source documentation

Cartan's contraction identity for the circle field, proved using actual Fréchet derivatives and circle invariance.

theorem extDeriv_circle_horizontal {a : E → E →L[ℝ] ℂ} {x : E} {q : ℂ}
    (ha : DifferentiableAt ℝ a x)
    (hinv : ∀ (t : ℝ) (w : E),
      a (circleMap 0 1 t • x) (circleMap 0 1 t • w) = a x w)
    (hconst : (fun y => a y (I • y)) =ᶠ[𝓝 x] (fun _ => q)) (w : E) :
    extDeriv (oneForm a) x ![I • x, w] = 0 := by
…

Mentions: OAI.Mahler.oneForm

lemma OAI.Mahler.contDiffAt_logTau_of_open line 111

Source documentation

C^2 regularity of log tau follows from first-order holomorphicity.

lemma contDiffAt_logTau_of_open [FiniteDimensional ℂ E]
    {ι : Type*} [Fintype ι] {f : ι → E → ℂ} {U : Set E} {x : E}
    (hU : IsOpen U) (hx : x ∈ U) (hf : ∀ j, DifferentiableOn ℂ (f j) U)
    (ht : 0 < tau f x) : ContDiffAt ℝ 2 (logTau f) x := by
…

Mentions: OAI.Mahler.tau, OAI.Mahler.logTau

lemma OAI.Mahler.differentiableAt_dcLinear line 126

lemma OAI.Mahler.dcLinear_rotation line 132

Source documentation

d^c respects the circle action when the scalar function does.

lemma dcLinear_rotation {u : E → ℂ} {x : E} {c : ℂ}
    (hu : DifferentiableAt ℝ u (c • x))
    (hinv : ∀ y, u (c • y) = u y) (w : E) :
    dcLinear u (c • x) (c • w) = dcLinear u x w := by
…

Mentions: OAI.Mahler.dcLinear

theorem OAI.Mahler.homogeneous_extDeriv_horizontal line 151

Source documentation

The homogeneous alpha has horizontal exterior derivative, with all regularity derived from holomorphicity.

theorem homogeneous_extDeriv_horizontal [FiniteDimensional ℂ E]
    {f : ι → E → ℂ} {x : E} {m : ℕ}
    (hf : ∀ j, Differentiable ℂ (f j)) (ht : 0 < tau f x)
    (hh : ∀ j (y : E) (c : ℂ), f j (c • y) = c^m * f j y) (w : E) :
    extDeriv (oneForm (dcLinear (logTau f))) x ![I • x, w] = 0 := by
…

Mentions: OAI.Mahler.tau, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau