OAI/NumberTheory/TotientAsymptotic/FordSimplexEmbedding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.a_one_lt_one line 14
2. lemma OAI.TotientAsymptotic.prefixRegion_nonneg line 18
3. def OAI.TotientAsymptotic.fordSimplex line 23
4. def OAI.TotientAsymptotic.shrinkLast line 27
5. lemma OAI.TotientAsymptotic.shrinkLast_apply line 30
6. lemma OAI.TotientAsymptotic.shrinkLast_det line 34
7. lemma OAI.TotientAsymptotic.shrinkLast_le line 38
8. theorem OAI.TotientAsymptotic.shrinkLast_mem_fordSimplex line 48

   Source documentation

   Scaling only the last coordinate by a₁ places our exact simplex inside Ford's S*. All earlier coordinates, hence their band events, are preserved.

   theorem shrinkLast_mem_fordSimplex {N : ℕ} {B : ℝ} {u : Fin (N+2) → ℝ}
       (hu : u ∈ prefixRegion (N+2) B 0 0) : shrinkLast N u ∈ fordSimplex N B := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.shrinkLast, OAI.TotientAsymptotic.fordSimplex

9. lemma OAI.TotientAsymptotic.shrinkLast_preserves_prefix line 110
10. theorem OAI.TotientAsymptotic.shrinkLast_volume_bound line 116

    Source documentation

    A measurable event in Ford's simplex bounds its preimage in our simplex, with only the fixed Jacobian factor 1/a₁.

    theorem shrinkLast_volume_bound {N : ℕ} {B : ℝ}
        (S T : Set (Fin (N+2) → ℝ)) (hT : MeasurableSet T)
        (hS : ∀ u ∈ S, u ∈ prefixRegion (N+2) B 0 0)
        (hST : ∀ u ∈ S, shrinkLast N u ∈ T) :
        volume S ≤ ENNReal.ofReal ((a 1)⁻¹)*volume (fordSimplex N B ∩ T) := by
    …

    Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.shrinkLast, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.fordSimplex