DilationTransport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.realDilation line 12
lemma OAI.Mahler.realDilation_apply line 14
lemma OAI.Mahler.dcLinear_dilation line 16
lemma OAI.Mahler.dcLinear_sub_const line 26
def OAI.Mahler.boundaryForm line 33
Source documentation
The full shuffle boundary form, using actual exterior differentiation.
```
noncomputable def boundaryForm (u : E → ℂ) (k : ℕ) (x : E) :
    E [⋀^Fin 1 ⊕ WedgePowerSlots k]→ₗ[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.WedgePowerSlots
lemma OAI.Mahler.oneForm_dilation_eventually line 38

theorem OAI.Mahler.extDeriv_dc_dilation line 51

Source documentation

Pullback of the actual dd^c under a real dilation.

theorem extDeriv_dc_dilation {u : E → ℂ} {r : ℝ} {x : E}
    (hu : ContDiffAt ℝ 2 u (r • x)) :
    extDeriv (oneForm (dcLinear (fun y => u (r • y)))) x =
      (extDeriv (oneForm (dcLinear u)) (r • x)).compContinuousLinearMap (realDilation r) := by
…

Mentions: OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.realDilation

theorem OAI.Mahler.boundaryForm_dilation line 66

Source documentation

Every tangent slot is transported by the derivative of dilation; the constant subtracted from the logarithm disappears from both derivatives.

theorem boundaryForm_dilation {u : E → ℂ} {r : ℝ} {x : E}
    (hu : ContDiffAt ℝ 2 u (r • x)) (c : ℂ) (k : ℕ) :
    boundaryForm (fun y => u (r • y) - c) k x =
      (boundaryForm u k (r • x)).compLinearMap (realDilation r).toLinearMap := by
…

Mentions: OAI.Mahler.boundaryForm, OAI.Mahler.realDilation