OAI/Analysis/Mahler/OpenExteriorNormalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.coordinateDirection line 11
2. lemma OAI.Mahler.linearMap_coordinate_expansion line 14
3. lemma OAI.Mahler.pairing_coordinate_expansion line 22
4. lemma OAI.Mahler.logKernel_coordinate_expansion line 41
5. lemma OAI.Mahler.extDeriv_energy_matrix_of_open line 63
6. lemma OAI.Mahler.extDeriv_logTau_matrix_of_open line 81
7. theorem OAI.Mahler.extDeriv_energy_top_of_open line 99

   Source documentation

   The top exterior normalization, under open-domain first-order holomorphicity, with no additional smoothness premise.

   theorem extDeriv_energy_top_of_open (hU : IsOpen U) (hx : x ∈ U)
       (hf : ∀ j, DifferentiableOn ℂ (f j) U) :
       wedgePower (extDeriv (oneForm (dcLinear (energy f))) x).toAlternatingMap n =
         ((n.factorial : ℂ) * (sourceHessian (energy f) x coordinateDirection).det) • interleavedVolume n := by
   …

   Mentions: OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.energy, OAI.Mahler.sourceHessian, OAI.Mahler.coordinateDirection, OAI.Mahler.interleavedVolume

8. theorem OAI.Mahler.extDeriv_logTau_top_of_open line 105
9. theorem OAI.Mahler.MassHypotheses.massDensity_eq_topForm line 113

   Source documentation

   The density already used by the exact mass target is the real coefficient of the actual top exterior form in the positive Euclidean coordinate frame.

   theorem MassHypotheses.massDensity_eq_topForm {N m : ℕ}
       {f : Fin N → ComplexEuclidean n → ℂ} {G : Fin N → MvPolynomial (Fin n) ℂ}
       (h : MassHypotheses n N m U f G) (hx : x ∈ U) :
       massDensity f x =
         (wedgePower (extDeriv (oneForm (dcLinear (energy f))) x).toAlternatingMap n
           interleavedBasis).re := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.massDensity, OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.energy, OAI.Mahler.interleavedBasis