OAI/NumberTheory/TotientAsymptotic/PrefixTerminalVolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The terminal slice of a prefix region is another prefix region.

  1. lemma OAI.TotientAsymptotic.prefixLinear_last line 11
  2. lemma OAI.TotientAsymptotic.weighted_sum_update_last line 21
  3. lemma OAI.TotientAsymptotic.prefixRegion_terminal_inter line 35
  4. theorem OAI.TotientAsymptotic.volume_prefixRegion_terminal line 62

    Source documentation

    Exact cap volume, including the empty-cap case through the positive part.

    theorem volume_prefixRegion_terminal (N : ℕ) (B C₀ : ℝ)
    (C : Fin (N+1) → ℝ) {t : ℝ} (ht : C (Fin.last N) ≤ t) :
    volume (prefixRegion (N+1) B C₀ C ∩ {u | t ≤ u (Fin.last N)})=
      ENNReal.ofReal
        ((max (B-C₀-(∑ i : Fin (N+1),g (i.val+1)*C i)-
            g (N+1)*(t-C (Fin.last N))) 0)^(N+1)/
          (((N+1).factorial:ℝ)*∏ i : Fin (N+1),g (i.val+1))) := by
…

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