MassTarget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Mahler.ComplexEuclidean line 12
structure OAI.Mahler.MassHypotheses line 16
Source documentation
The hypotheses for the isolated-zero mass inequality. This structure records hypotheses; it does not assert the inequality.
```
structure MassHypotheses (n N m : ℕ) (U : Set (ComplexEuclidean n))
    (f : Fin N → ComplexEuclidean n → ℂ)
    (G : Fin N → MvPolynomial (Fin n) ℂ) : Prop where
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.Mahler.massDensity line 36
Source documentation
The density n! det(tau_{z_k bar z_l}) for the complex Hessian convention.
```
noncomputable def massDensity {n N : ℕ} (f : Fin N → ComplexEuclidean n → ℂ)
    (z : ComplexEuclidean n) : ℝ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.Mahler.massIntegral line 43
Source documentation
The extended nonnegative integral allows infinite mass. This definition does not assert its equality to an exterior-form integral.
```
noncomputable def massIntegral {n N : ℕ} (U : Set (ComplexEuclidean n))
    (f : Fin N → ComplexEuclidean n → ℂ) : ℝ≥0∞ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.Mahler.MassBoundTarget line 47