OAI/Analysis/Mahler/SourceHomogeneous.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.eval_homogeneous_scale line 15

   Source documentation

   Conversion from the polynomial homogeneity predicate to its scaling equation; no functional homogeneity assumption is added.

   lemma eval_homogeneous_scale {σ : Type*} {p : MvPolynomial σ ℂ} {m : ℕ}
       (hp : p.IsHomogeneous m) (z : σ → ℂ) (c : ℂ) :
       MvPolynomial.eval (fun i => c * z i) p = c ^ m * MvPolynomial.eval z p := by
   …

2. def OAI.Mahler.polynomialMap line 28
3. lemma OAI.Mahler.polynomialMap_differentiable line 31
4. lemma OAI.Mahler.polynomialMap_homogeneous line 40
5. lemma OAI.Mahler.tau_pos_of_component_ne_zero line 47
6. theorem OAI.Mahler.MassHypotheses.homogeneous_extDeriv_horizontal line 56

   Source documentation

   The original mass hypotheses imply horizontality of the actual homogeneous exterior derivative at every nonzero point.

   theorem MassHypotheses.homogeneous_extDeriv_horizontal {n N m : ℕ}
       {U : Set (ComplexEuclidean n)} {f : Fin N → ComplexEuclidean n → ℂ}
       {G : Fin N → MvPolynomial (Fin n) ℂ} (h : MassHypotheses n N m U f G)
       {z : ComplexEuclidean n} (hz : z ≠ 0) (v : ComplexEuclidean n) :
       extDeriv (oneForm (dcLinear (logTau (polynomialMap G)))) z ![I • z, v] = 0 :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.Mahler.polynomialMap