OAI/NumberTheory/TotientAsymptotic/SimplexScaling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.enlargedSimplex line 13
2. def OAI.TotientAsymptotic.simplexScale line 18
3. lemma OAI.TotientAsymptotic.simplexScale_apply line 21
4. lemma OAI.TotientAsymptotic.simplexScale_det line 25
5. lemma OAI.TotientAsymptotic.enlargedSimplex_mapsTo line 29
6. theorem OAI.TotientAsymptotic.volume_enlargedSimplex_le line 68

   Source documentation

   The Jacobian cost is the product of the coordinate scaling factors.

   theorem volume_enlargedSimplex_le {N : ℕ} (B β₀ : ℝ) (β κ : Fin N → ℝ)
       (hβ₀ : 0 < β₀) (hβ : ∀ i, 0 < β i) (hκ : ∀ i, 0 < κ i)
       (htop : ∀ i, β₀ ≤ κ i) (hstep : ∀ i j, i < j → β i*κ i ≤ κ j) :
       volume (enlargedSimplex N B β₀ β) ≤
         ENNReal.ofReal (∏ i, κ i)*volume (prefixRegion N B 0 0) := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.prefixRegion

7. def OAI.TotientAsymptotic.enlargementScale line 86
8. lemma OAI.TotientAsymptotic.enlargementScale_pos line 89
9. lemma OAI.TotientAsymptotic.enlargementScale_top line 93
10. lemma OAI.TotientAsymptotic.enlargementScale_step line 103
11. theorem OAI.TotientAsymptotic.volume_enlargedSimplex_product_bound line 115