DCForms.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.complexStructure line 16
Source documentation
Multiplication by i, viewed as a real continuous linear map.
```
def complexStructure : E →L[ℝ] E :=
…
```
def OAI.MahlerStokes.dcForm line 20
Source documentation
The operator d^c as a real alternating one-form.
```
def dcForm (g : E → ℝ) (x : E) : E [⋀^Fin 1]→L[ℝ] ℝ :=
…
```
lemma OAI.MahlerStokes.dcForm_apply line 24
theorem OAI.MahlerStokes.dcForm_complex_coe line 29

theorem OAI.MahlerStokes.dcForm_log line 38

Source documentation

The identity d^c log g = g^{-1} d^c g, with the real logarithm.

theorem dcForm_log {g : E → ℝ} {x : E} (hg : DifferentiableAt ℝ g x) (hp : 0 < g x) :
    dcForm (fun y => Real.log (g y)) x = (g x)⁻¹ • dcForm g x := by
…

Mentions: OAI.MahlerStokes.dcForm

def OAI.MahlerStokes.pullbackForm line 51
Source documentation
The usual pullback, defined using the actual derivative of the parametrization.
```
def pullbackForm {k : ℕ} (φ : V → E) (ω : E → E [⋀^Fin k]→L[ℝ] ℝ)
    (y : V) : V [⋀^Fin k]→L[ℝ] ℝ :=
…
```

theorem OAI.MahlerStokes.pullback_dc_log_level line 56

Source documentation

On a level parametrization, the actual pulled-back one-form scales by R^{-1}.

theorem pullback_dc_log_level {φ : V → E} {g : E → ℝ} {R : ℝ} {y : V}
    (hR : 0 < R) (hg : DifferentiableAt ℝ g (φ y)) (hlevel : g (φ y) = R) :
    pullbackForm φ (dcForm (fun x => Real.log (g x))) y =
      R⁻¹ • pullbackForm φ (dcForm g) y := by
…

Mentions: OAI.MahlerStokes.pullbackForm, OAI.MahlerStokes.dcForm

theorem OAI.MahlerStokes.extDeriv_pullback_dc_log_level line 67

Source documentation

Taking the actual exterior derivative on a level chart preserves the same factor. This uses a proved local equality, not a Stokes assumption.

theorem extDeriv_pullback_dc_log_level {φ : V → E} {g : E → ℝ} {R : ℝ} {s : Set V} {y : V}
    (hs : IsOpen s) (hy : y ∈ s) (hR : 0 < R)
    (hg : ∀ z ∈ s, DifferentiableAt ℝ g (φ z)) (hlevel : ∀ z ∈ s, g (φ z) = R) :
    extDeriv (pullbackForm φ (dcForm (fun x => Real.log (g x)))) y =
      R⁻¹ • extDeriv (pullbackForm φ (dcForm g)) y := by
…

Mentions: OAI.MahlerStokes.pullbackForm, OAI.MahlerStokes.dcForm

theorem OAI.MahlerStokes.pullback_ddc_log_level line 81

Source documentation

Boundary restriction of dd^c log g: the pullback of the exterior derivative is R^{-1} times that of dd^c g.

theorem pullback_ddc_log_level {φ : V → E} {g : E → ℝ} {R : ℝ} {s : Set V} {y : V}
    (hs : IsOpen s) (hy : y ∈ s) (hR : 0 < R)
    (hg : ∀ z ∈ s, DifferentiableAt ℝ g (φ z)) (hlevel : ∀ z ∈ s, g (φ z) = R)
    (hφ : ContDiffAt ℝ 2 φ y)
    (hdc : DifferentiableAt ℝ (dcForm g) (φ y))
    (hlog : DifferentiableAt ℝ (dcForm (fun x => Real.log (g x))) (φ y)) :
    pullbackForm φ (extDeriv (dcForm (fun x => Real.log (g x)))) y =
      R⁻¹ • pullbackForm φ (extDeriv (dcForm g)) y := by
…

Mentions: OAI.MahlerStokes.dcForm, OAI.MahlerStokes.pullbackForm