LineSmoothness.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth points and gradients of line arrangements

def OAI.Nagata.W06.LineArrangement.planeEval line 28
Source documentation
Evaluation of an actual bivariate polynomial at affine coordinates (U,Y).
```
def planeEval {K : Type*} [CommRing K] (P : Polynomial (Polynomial K)) (U Y : K) : K :=
…
```

theorem OAI.Nagata.W06.LineArrangement.derivative_prod_eval₂_root line 32

Source documentation

Product-rule identity at a chosen root, valid before any nonvanishing assumption.

theorem derivative_prod_eval₂_root {A B ι : Type*} [CommRing A] [CommRing B]
    [Fintype ι] [DecidableEq ι] (f : A →+* B) (a : ι → A) (i : ι) :
    (∏ j : ι, (X - C (a j))).derivative.eval₂ f (f (a i)) =
      ∏ j ∈ Finset.univ.erase i, (f (a i) - f (a j)) := by
…

theorem OAI.Nagata.W06.LineArrangement.eval_affineLineGraph line 43
theorem OAI.Nagata.W06.LineArrangement.planeEval_lineUnion line 48
Source documentation
The actual reduced curve equation evaluates to the product of its line equations.
```
theorem planeEval_lineUnion (k : ℕ) (U Y : K) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k) U Y =
      ∏ i : Fin k, lineValue i.val U Y := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.lineValue
theorem OAI.Nagata.W06.LineArrangement.lineUnion_zero_at_mark line 61
Source documentation
Each of the displayed marked points lies on the actual reduced curve equation.
```
theorem lineUnion_zero_at_mark (k : ℕ) (i s : Fin k) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k)
      (markedPoint K k i s).1 (markedPoint K k i s).2 = 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.markedPoint
theorem OAI.Nagata.W06.LineArrangement.partialY_lineUnion_negative_mark line 71
Source documentation
At any negative-U point on component i, the Y-partial derivative of the entire line union is nonzero. All the other line factors are nonzero there.
```
theorem partialY_lineUnion_negative_mark (k : ℕ) (i : Fin k) (v : ℕ) (hv : 0 < v) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
      (-(v : K)) (graphValue i.val (-(v : K))) ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.graphValue
theorem OAI.Nagata.W06.LineArrangement.partialY_lineUnion_at_mark line 92
Source documentation
The concrete nonzero Y-partial derivative at every one of the k² marks.
```
theorem partialY_lineUnion_at_mark (k : ℕ) (i s : Fin k) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
      (markedPoint K k i s).1 (markedPoint K k i s).2 ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.markedPoint

theorem OAI.Nagata.W06.LineArrangement.markedPoint_nonsingular_certificate line 99

Source documentation

A genuine equation/derivative nonsingularity certificate for all marked points.

theorem markedPoint_nonsingular_certificate (k : ℕ) (i s : Fin k) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k)
        (markedPoint K k i s).1 (markedPoint K k i s).2 = 0 ∧
      planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
        (markedPoint K k i s).1 (markedPoint K k i s).2 ≠ 0 :=
…

Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.markedPoint

theorem OAI.Nagata.W06.LineArrangement.line_arrangement_marked_configuration line 108
Source documentation
The explicit k²-point configuration with its actual hypersurface certificates. The formula is valid for every k, in particular every k≥4.
```
theorem line_arrangement_marked_configuration (k : ℕ) :
    (markedPoints K k).card = k ^ 2 ∧
      ∀ p ∈ markedPoints K k,
        planeEval (Nagata.Workers.W24.lineUnionEquation K k) p.1 p.2 = 0 ∧
        planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative p.1 p.2 ≠ 0 := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.markedPoints, OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation

theorem OAI.Nagata.W06.LineArrangement.additionalPoint_nonsingular_certificate line 120

Source documentation

The extra point is also on the actual curve and has nonzero Y-partial derivative.

theorem additionalPoint_nonsingular_certificate (k : ℕ) (hk : 0 < k) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k)
        (additionalPoint K k).1 (additionalPoint K k).2 = 0 ∧
      planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
        (additionalPoint K k).1 (additionalPoint K k).2 ≠ 0 := by
…

Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.additionalPoint

theorem OAI.Nagata.W06.LineArrangement.exists_vertical_displacement_scalar line 132
Source documentation
Every target scalar of the actual vertical polynomial differential at the extra point is attained.
```
theorem exists_vertical_displacement_scalar (k : ℕ) (hk : 0 < k) (c : K) :
    ∃ t : K,
      planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
        (additionalPoint K k).1 (additionalPoint K k).2 * t = c := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.additionalPoint

theorem OAI.Nagata.W06.LineArrangement.line_arrangement_with_additional_point line 142

Source documentation

The complete k²+1 configuration, including the extra point required by the triangle case.

theorem line_arrangement_with_additional_point (k : ℕ) (hk : 0 < k) :
    (extendedMarkedPoints K k).card = k ^ 2 + 1 ∧
      ∀ p ∈ extendedMarkedPoints K k,
        planeEval (Nagata.Workers.W24.lineUnionEquation K k) p.1 p.2 = 0 ∧
        planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative p.1 p.2 ≠ 0 := by
…

Mentions: OAI.Nagata.W06.LineArrangement.extendedMarkedPoints, OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation