MarkedPoints.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Choice of nine distinct marked parameters avoiding integral displacements

theorem OAI.Nagata.W06.exists_between_avoiding_finite line 22
Source documentation
Every nonempty real interval contains a point outside any given finite set.
```
theorem exists_between_avoiding_finite {a b : ℝ} (hab : a < b)
    {F : Set ℝ} (hF : F.Finite) : ∃ x, a < x ∧ x < b ∧ x ∉ F := by
…
```

theorem OAI.Nagata.W06.exists_delta_avoiding_finite line 44

Source documentation

The manuscript's strict delta slack survives deletion of a finite set.

theorem exists_delta_avoiding_finite {ρ B : ℝ} (hρ : 0 < ρ) (hB : ρ < B)
    {F : Set ℝ} (hF : F.Finite) :
    ∃ Δ : ℝ, 0 < Δ ∧ Δ < 1 / 2 ∧ ρ + Δ * ρ / 9 < B ∧ Δ ∉ F := by
…

def OAI.Nagata.W06.nineDisplacement line 70
Source documentation
Positive arithmetic-progression displacements of total Δ.
```
noncomputable def nineDisplacement (Δ : ℝ) (i : Fin 9) : ℝ := Δ * ((i.val : ℝ) + 1) / 45
```
def OAI.Nagata.W06.markedExponent line 73
Source documentation
Exponents for the nine marked points in the manuscript.
```
noncomputable def markedExponent (Δ : ℝ) (i : Fin 9) : ℝ := 1 / 2 - nineDisplacement Δ i
```
Mentions: OAI.Nagata.W06.nineDisplacement
theorem OAI.Nagata.W06.nineDisplacement_pos line 75
theorem OAI.Nagata.W06.nineDisplacement_lt line 80
theorem OAI.Nagata.W06.nineDisplacement_injective line 87
theorem OAI.Nagata.W06.sum_nineDisplacement line 96
theorem OAI.Nagata.W06.markedExponent_pos line 101
theorem OAI.Nagata.W06.markedExponent_lt_half line 107
theorem OAI.Nagata.W06.markedExponent_injective line 113
theorem OAI.Nagata.W06.sum_markedExponent_displacement line 120

theorem OAI.Nagata.W06.exists_marked_parameters line 125

Source documentation

The complete real-parameter existence assertion of marked-parameters.

theorem exists_marked_parameters {Δ : ℝ} (hΔ : 0 < Δ) (hhalf : Δ < 1 / 2) :
    ∃ x : Fin 9 → ℝ, Function.Injective x ∧
      (∀ i, 0 < x i ∧ x i < 1 / 2) ∧
      ∑ i : Fin 9, (1 / 2 - x i) = Δ := by
…

theorem OAI.Nagata.W06.eq_of_sub_eq_integer line 135

Source documentation

Exponents inside one open unit interval cannot differ by a nonzero integer.

theorem eq_of_sub_eq_integer {x y : ℝ} (hx0 : 0 < x) (hx1 : x < 1)
    (hy0 : 0 < y) (hy1 : y < 1) (k : ℤ) (hk : x - y = k) : x = y := by
…

theorem OAI.Nagata.W06.markedExponent_difference_not_integer line 148

Source documentation

Distinct marked exponents are distinct modulo integer translation.

theorem markedExponent_difference_not_integer {Δ : ℝ} (hΔ : 0 < Δ)
    (hhalf : Δ < 1 / 2) {i j : Fin 9} (hij : i ≠ j) (k : ℤ) :
    markedExponent Δ i - markedExponent Δ j ≠ k := by
…

Mentions: OAI.Nagata.W06.markedExponent