OAI/Analysis/Mahler/HomogeneousDeformation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.betaLinear line 14

   Source documentation

   The deformation beta, represented as a real-linear one-form.

   noncomputable def betaLinear (f : ι → E → ℂ) (g : κ → E → ℂ) (m : ℕ)
       (x : E) : E →L[ℝ] ℂ := dcLinear (logTau f) x - (m : ℝ) • dcLinear (logTau g) x

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

2. def OAI.Mahler.alphaPath line 18

   Source documentation

   The actual one-form alpha_t = m alpha_0 + t beta.

   noncomputable def alphaPath (f : ι → E → ℂ) (g : κ → E → ℂ) (m : ℕ)
       (t : ℝ) (x : E) : E →L[ℝ] ℂ :=
   …

3. lemma OAI.Mahler.betaLinear_circle line 23
4. lemma OAI.Mahler.betaLinear_eq_dc line 36

   Source documentation

   The bundled beta is exactly d^c(log T - m log |z|^2) when g is the coordinate map.

   lemma betaLinear_eq_dc [FiniteDimensional ℂ E] {f : ι → E → ℂ} {g : κ → E → ℂ} {x : E} {m : ℕ}
       (hf : ∀ j, DifferentiableAt ℂ (f j) x) (htf : 0 < tau f x)
       (hg : ∀ j, DifferentiableAt ℂ (g j) x) (htg : 0 < tau g x) (v : E) :
       betaLinear f g m x v = dc (fun y => logTau f y - (m : ℂ) * logTau g y) x v := by
   …

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

5. lemma OAI.Mahler.alphaPath_circle line 46
6. lemma OAI.Mahler.homogeneous_dcLinear_rotation line 58
7. lemma OAI.Mahler.tau_continuousAt line 70
8. theorem OAI.Mahler.alphaPath_extDeriv_horizontal line 77

   Source documentation

   Circle horizontality for the actual whole deformation, for every real t. The only regularity hypotheses are first-order holomorphicity.

   theorem alphaPath_extDeriv_horizontal {f : ι → E → ℂ} {g : κ → E → ℂ}
       {x : E} {m : ℕ}
       (hf : ∀ j, Differentiable ℂ (f j)) (htf : 0 < tau f x)
       (hfg : ∀ j (y : E) (c : ℂ), f j (c • y) = c^m * f j y)
       (hg : ∀ j, Differentiable ℂ (g j)) (htg : 0 < tau g x)
       (hgg : ∀ j (y : E) (c : ℂ), g j (c • y) = c^1 * g j y)
       (t : ℝ) (v : E) :
       extDeriv (oneForm (alphaPath f g m t)) x ![I • x, v] = 0 := by
   …

   Mentions: OAI.Mahler.tau, OAI.Mahler.oneForm, OAI.Mahler.alphaPath