ArithmeticReduction.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Factorial dilation and square arithmetic reductions

theorem OAI.Nagata.Workers.W14.multiplicity_sum_pos line 21
Source documentation
A violating multiplicity sum is positive when the degree and point count are positive.
```
theorem multiplicity_sum_pos {r d s : ℕ} (hr : 0 < r) (hd : 0 < d)
    (h : (d : ℝ) * Real.sqrt r ≤ s) : 0 < s := by
…
```

theorem OAI.Nagata.Workers.W14.symmetrized_ratio_le line 30

Source documentation

The scalar ratio estimate underlying symmetrization.

theorem symmetrized_ratio_le {r d s : ℕ} (hs : 0 < s)
    (h : (d : ℝ) * Real.sqrt r ≤ s) :
    (r : ℝ) * d / s ≤ Real.sqrt r := by
…

theorem OAI.Nagata.Workers.W14.factorial_ratio_eq line 45

Source documentation

Cancel the factorial that occurs in every point's multiplicity.

theorem factorial_ratio_eq {r d s : ℕ} (hr : 0 < r) (hs : 0 < s) :
    ((r.factorial * d : ℕ) : ℝ) / (((r - 1).factorial * s : ℕ) : ℝ) =
      (r : ℝ) * d / s := by
…

theorem OAI.Nagata.Workers.W14.factorial_symmetrization line 57

Source documentation

Exact positive degree and common multiplicity produced by the permutation product.

theorem factorial_symmetrization {r d s : ℕ} (hr : 0 < r) (hd : 0 < d)
    (h : (d : ℝ) * Real.sqrt r ≤ s) :
    0 < r.factorial * d ∧ 0 < (r - 1).factorial * s ∧
      ((r.factorial * d : ℕ) : ℝ) / (((r - 1).factorial * s : ℕ) : ℝ) ≤
        Real.sqrt r := by
…

theorem OAI.Nagata.Workers.W14.common_power_ratio line 69
Source documentation
Taking common positive powers preserves the degree to multiplicity ratio.
```
theorem common_power_ratio (d m N : ℕ) (hN : 0 < N) :
    ((N * d : ℕ) : ℝ) / ((N * m : ℕ) : ℝ) = (d : ℝ) / m := by
…
```
theorem OAI.Nagata.Workers.W14.ratio_ne_sqrt_of_nonsquare line 84
Source documentation
For nonsquare point counts a rational homogeneous slope cannot equal the boundary.
```
theorem ratio_ne_sqrt_of_nonsquare (r d m : ℕ) (hr : ¬ IsSquare r) :
    (d : ℝ) / m ≠ Real.sqrt r := by
…
```

theorem OAI.Nagata.Workers.W14.ratio_lt_sqrt_of_nonsquare line 96

Source documentation

Consequently a weak homogeneous bound is strict for nonsquare r.

theorem ratio_lt_sqrt_of_nonsquare {r d m : ℕ} (hr : ¬ IsSquare r)
    (h : (d : ℝ) / m ≤ Real.sqrt r) : (d : ℝ) / m < Real.sqrt r :=
…

theorem OAI.Nagata.Workers.W14.elliptic_ratio_range line 101

Source documentation

The two numerical exclusions put the homogeneous slope in the elliptic range.

theorem elliptic_ratio_range {r d m : ℕ} (hr : ¬ IsSquare r) (hm : 0 < m)
    (hlow : 3 * m < d) (hhigh : (d : ℝ) / m ≤ Real.sqrt r) :
    3 < (d : ℝ) / m ∧ (d : ℝ) / m < Real.sqrt r := by
…

theorem OAI.Nagata.Workers.W14.sqrt_nat_square line 118
Source documentation
The positive square root of a natural square is its natural root.
```
theorem sqrt_nat_square (k : ℕ) : Real.sqrt ((k * k : ℕ) : ℝ) = k := by
…
```
theorem OAI.Nagata.Workers.W14.sqrt_nat_eq_iff line 122
Source documentation
An equality with a natural square root is equivalent to equality of squares.
```
theorem sqrt_nat_eq_iff (r k : ℕ) : Real.sqrt (r : ℝ) = k ↔ r = k * k := by
…
```
theorem OAI.Nagata.Workers.W14.square_root_ge_four line 132
Source documentation
A square point count at least ten has root at least four.
```
theorem square_root_ge_four {r k : ℕ} (hr : 10 ≤ r) (hk : r = k * k) : 4 ≤ k := by
…
```
theorem OAI.Nagata.Workers.W14.square_ratio_le_iff line 139
Source documentation
For a positive denominator the weak square bound is exactly the integral bound.
```
theorem square_ratio_le_iff {r k d m : ℕ} (hk : r = k * k) (hm : 0 < m) :
    (d : ℝ) / m ≤ Real.sqrt r ↔ d ≤ k * m := by
…
```