OAI/Analysis/Mahler/HomogeneousFlux.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.dc line 13

   Source documentation

   The convention d^c u(v) = -D_R u(iv)/4.

   noncomputable def dc (u : E → ℂ) (x v : E) : ℂ := -fderiv ℝ u x (I • v) / 4
   …

2. lemma OAI.Mahler.dc_circle line 16
3. lemma OAI.Mahler.dbar_real line 21
4. lemma OAI.Mahler.homogeneous_euler line 28

   Source documentation

   Euler's identity derived by differentiating the homogeneous scaling identity.

   lemma homogeneous_euler [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] {f : E → ℂ} {x : E} {m : ℕ}
       (hf : DifferentiableAt ℂ f x) (hh : ∀ c : ℂ, f (c • x) = c^m * f x) :
       fderiv ℂ f x x = (m : ℂ) * f x := by
   …

5. lemma OAI.Mahler.differentiable_logTau line 43
6. lemma OAI.Mahler.dz_logTau_radial line 53
7. theorem OAI.Mahler.homogeneous_dc_circle line 66

   Source documentation

   The homogeneous sphere-flux normalization alpha(V)=m/2, V(z)=iz.

   theorem homogeneous_dc_circle {f : ι → E → ℂ} {x : E} {m : ℕ}
       (hf : ∀ j, DifferentiableAt ℂ (f j) x) (ht : 0 < tau f x)
       (hh : ∀ j (c : ℂ), f j (c • x) = c^m * f j x) :
       dc (logTau f) x (I • x) = (m : ℂ) / 2 := by
   …

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

8. lemma OAI.Mahler.dc_sub line 76
9. lemma OAI.Mahler.dc_const_mul line 86
10. theorem OAI.Mahler.homogeneous_beta_circle line 97

    Source documentation

    The beta in the homogeneous flux argument annihilates the circle direction. The comparison map g has degree one; in particular, it can be the coordinate identity map.

    theorem homogeneous_beta_circle {κ : Type*} [Fintype κ]
        {f : ι → E → ℂ} {g : κ → E → ℂ} {x : E} {m : ℕ}
        (hf : ∀ j, DifferentiableAt ℂ (f j) x) (htf : 0 < tau f x)
        (hfg : ∀ j (c : ℂ), f j (c • x) = c^m * f j x)
        (hg : ∀ j, DifferentiableAt ℂ (g j) x) (htg : 0 < tau g x)
        (hgg : ∀ j (c : ℂ), g j (c • x) = c^1 * g j x) :
        dc (fun y => logTau f y - (m : ℂ) * logTau g y) x (I • x) = 0 := by
    …

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

11. lemma OAI.Mahler.tau_homogeneous line 113

    Source documentation

    Scaling of the actual squared norm follows from component homogeneity.

    lemma tau_homogeneous [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] {f : ι → E → ℂ} {x : E} {m : ℕ}
        (hh : ∀ j (c : ℂ), f j (c • x) = c^m * f j x) (c : ℂ) :
        tau f (c • x) = normSq c ^ m * tau f x := by
    …

    Mentions: OAI.Mahler.tau

12. lemma OAI.Mahler.logTau_circle_invariant line 119

    Source documentation

    Circle invariance is derived from homogeneity, not assumed.

    lemma logTau_circle_invariant {f : ι → E → ℂ} {x : E} {m : ℕ}
        (hh : ∀ j (c : ℂ), f j (c • x) = c^m * f j x)
        {c : ℂ} (hc : normSq c = 1) : logTau f (c • x) = logTau f x := by
    …

    Mentions: OAI.Mahler.logTau