OAI/NumberTheory/Ostmann/Construction/SmoothGiantTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_giant_diagonal_nonneg line 12

   Source documentation

   Positivity is established before estimating the ordered counterparts.

   theorem moving_giant_diagonal_nonneg {Y A : Type*} [Fintype Y] [Fintype A]
       (I : Finset ℕ) (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (U : Y → ℕ)
       (w : ℕ → ℝ) (hw : ∀ p ∈ I, 0 ≤ w p)
       (L : Y → A → ℕ) (v : Y → A → ℤ) (c : Y → ℕ → A → ℂ)
       (hpos : ∀ y p, p ∈ I → ∀ a, c y p a ≠ 0 → 0 < L y a) :
       0 ≤ ∑ y, μ y * (U y : ℝ) *
         ∑ p ∈ I, w p * (pivotDiagonal (L y) (v y) (c y p)).re := by
   …

   Mentions: OAI.Ostmann.pivotDiagonal

2. theorem OAI.Ostmann.smoothGiantPrior_transfer line 30

   Source documentation

   The actual normalizer of (7.3), not a factorial or an assumed transfer loss, gives the loss in (7.13). The off-diagonal on the right is the exact weighted positive-integer substitution.

   theorem smoothGiantPrior_transfer {Y A : Type*} [Fintype Y] [Fintype A]
       (P I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPI : P ⊆ I)
       (hI : ∀ p ∈ I, 0 < p)
       (φ : ℝ → ℝ) (G : ℝ) (hφ : ∀ x, 0 ≤ φ x)
       (hpos : 0 < smoothGiantMass P φ G)
       (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hμmass : ∑ y, μ y = 1)
       (U : Y → ℕ) (hU : ∀ y, 0 < U y)
       (row : ∀ y, (p : P) → Fin ((p : ℕ) * U y) → ℂ)
       (hrow : ∀ y p, (∑ t, ‖row y p t‖ ^ 2) ≤ (p : ℕ) * (U y : ℝ))
       (L : Y → A → ℕ) (v : Y → A → ℤ) (c : Y → ℕ → A → ℂ)
       (hcoprime : ∀ y p, p ∈ I → ∀ a, c y p a ≠ 0 → (L y a).Coprime (p * U y))
       (N H V : ℕ)
   …

   Mentions: OAI.Ostmann.smoothGiantMass