OAI/Analysis/Mahler/HomogeneousSphereIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.boundaryFormFin_smul line 10
2. def OAI.Mahler.homogeneousPathFlux line 28

   Source documentation

   The flux along the one-form deformation.

   noncomputable def homogeneousPathFlux (k N m : ℕ)
       (G : Fin N → MvPolynomial (Fin (k+1)) ℂ) (t : ℝ) : ℝ :=
   …

3. def OAI.Mahler.homogeneousSphereFlux line 33

   Source documentation

   The actual homogeneous endpoint, with no flux-constancy premise.

   noncomputable def homogeneousSphereFlux (k N : ℕ)
       (G : Fin N → MvPolynomial (Fin (k+1)) ℂ) : ℝ :=
   …

4. lemma OAI.Mahler.alphaPath_zero line 37
5. lemma OAI.Mahler.alphaPath_one line 45
6. theorem OAI.Mahler.homogeneousPathFlux_zero line 52
7. lemma OAI.Mahler.homogeneousPathFlux_one line 70