Exact incidence averaging over every affine-plane parameter triple, including degenerate triples. No divisibility correction for plane charts is needed because points and directions are kept as coordinates.
def
CCDN.PlaneSectionPoints
{K : Type u_1}
{σ : Type u_2}
[CommRing K]
(f : MvPolynomial σ K)
(v : PlaneParameters σ → K)
:
Type u_1
All plane coordinates whose image lies on the hypersurface.
Equations
- CCDN.PlaneSectionPoints f v = { t : Fin 2 → K // (CCDN.bivariateEval (t 0) (t 1)) (CCDN.universalPlaneSection f v) = 0 }
Instances For
theorem
CCDN.sum_planeSectionPoints_card
{K : Type u_1}
{σ : Type u_2}
[CommRing K]
[Fintype K]
[Fintype σ]
[DecidableEq σ]
(f : MvPolynomial σ K)
:
∑ v : PlaneParameters σ → K, Nat.card (PlaneSectionPoints f v) = Nat.card { z : σ → K // (MvPolynomial.eval z) f = 0 } * Fintype.card K ^ (2 * Fintype.card σ + 2)
The section counts sum to the exact incidence count.