ScaledMatrices.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scaled theta jet matrices and noncancellation

theorem OAI.Nagata.W29.exists_scaled_thetaJetMatrix_source_data line 18

theorem OAI.Nagata.W29.exists_scaled_thetaJetMatrix_injective line 71

Source documentation

A shorter consequence of the full simultaneous source-data package.

theorem exists_scaled_thetaJetMatrix_injective
    (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) :
    ∃ (n : ℕ) (delta : ℝ) (x : Fin 9 → ℝ),
      0 < n ∧ 0 < delta ∧ delta < 1 / 2 ∧
      Function.Injective x ∧ (∀ i, 0 < x i ∧ x i < 1 / 2) ∧
      (∑ i : Fin 9, sourceOffsets x i) = delta ∧
      ∀ᶠ τ in 𝓝[>] (0 : ℝ), Function.Injective
        (Nagata.Workers.W11.thetaJetMatrix ((n * d : ℕ) : ℤ) (r - 9) (n * m)
          (3 * (Real.sqrt r - 3)) delta (sourceOffsets x) τ).mulVec := by
…

Mentions: OAI.Nagata.W29.sourceOffsets, OAI.Nagata.Workers.W11.thetaJetMatrix

theorem OAI.Nagata.W29.exists_scaled_thetaJetMatrix_kernel_obstruction line 87

Source documentation

An eventual nonzero kernel contradicts injectivity for the selected scalar matrix.

theorem exists_scaled_thetaJetMatrix_kernel_obstruction
    (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) :
    ∃ (n : ℕ) (delta : ℝ) (x : Fin 9 → ℝ),
      0 < n ∧ 0 < delta ∧ delta < 1 / 2 ∧
      Function.Injective x ∧ (∀ i, 0 < x i ∧ x i < 1 / 2) ∧
      (∑ i : Fin 9, sourceOffsets x i) = delta ∧
      ¬ (∀ᶠ τ in 𝓝[>] (0 : ℝ), ∃ v :
        Nagata.FiniteExponents.Column ((n * d : ℕ) : ℤ) ((n * m : ℕ) : ℤ)
          (3 * (Real.sqrt r - 3)) delta → ℂ,
        v ≠ 0 ∧
          (Nagata.Workers.W11.thetaJetMatrix ((n * d : ℕ) : ℤ) (r - 9) (n * m)
…

Mentions: OAI.Nagata.W29.sourceOffsets, OAI.Nagata.FiniteExponents.Column, OAI.Nagata.Workers.W11.thetaJetMatrix