OAI/NumberTheory/Ostmann/Construction/SignedBulkGain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.signedBulkGainTarget line 11
2. theorem OAI.Ostmann.signedBulkGainTarget_pos line 14
3. theorem OAI.Ostmann.signedBulkGainTarget_absorbs line 17
4. theorem OAI.Ostmann.signedBulkGainTarget_bound line 29

   Source documentation

   The actual number of bulk positions is 2^n*m, while the gain is multiplied once for each of the m spectator primes.

   theorem signedBulkGainTarget_bound (n m : ℕ) (C D W A δ : ℝ)
       (hW : 0 ≤ W) (hA : 0 ≤ A) (hδ : 0 ≤ δ)
       (hamp : A ≤ Real.exp (C * m)) (hgain : δ ≤ signedBulkGainTarget n C D) :
       (W * A) * 4 ^ Fintype.card (TreeLeafIndex n × Fin m) * δ ^ m ≤
         W * Real.exp (-D * m) := by
   …

   Mentions: OAI.Ostmann.signedBulkGainTarget, OAI.Ostmann.TreeLeafIndex

5. theorem OAI.Ostmann.exists_signedBulkGain_parameters line 47

   Source documentation

   One fixed mixed-Fourier tolerance and one prime threshold give the gain needed for any requested exponential rate, uniformly in the bulk length.

   theorem exists_signedBulkGain_parameters (n : ℕ) (C D : ℝ) :
       ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧ ∃ N : ℕ, 3 ≤ N ∧
         ∀ p : ℕ, N ≤ p →
           3 / Real.sqrt (p : ℝ) ≤ ε ∧
           quartetTreeConstant n * (ε ^ 2 + Real.sqrt (3 / (p : ℝ))) ≤
             (signedBulkGainTarget (n + 2) C D) ^ 2 := by
   …

   Mentions: OAI.Ostmann.quartetTreeConstant, OAI.Ostmann.signedBulkGainTarget