AdditiveShellUnion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summing all retained slack slices in one enlarged full-dimensional simplex.

def OAI.TotientAsymptotic.additiveBoxSimplex line 14
def OAI.TotientAsymptotic.additiveBoxShell line 17
lemma OAI.TotientAsymptotic.additiveBoxSimplex_volume_ne_top line 25
lemma OAI.TotientAsymptotic.additiveBoxShell_volume_ne_top line 30
theorem OAI.TotientAsymptotic.additiveBoxShell_volume_bound line 42
Source documentation
The union of all retained coordinate slices costs their sum, not the number of tail witnesses or full-dimensional boxes.
```
theorem additiveBoxShell_volume_bound {x : ℝ} {R N : ℕ}
    (hB : 0 < B x) (hN : 0 < N) (hRN : R ≤ N) :
    volume.real (additiveBoxShell x R N hRN) ≤
      (2*(N : ℝ)/B x*(boxTopError x+
        ∑ i : Fin R, g (i.val+1)*boxSlackError x (i.val+1)))*
      Real.exp ((N : ℝ)/B x*(boxTopError x+
        ∑ i : Fin N, g (i.val+1)*boxSlackError x (i.val+1)))*G x N := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.additiveBoxShell, OAI.TotientAsymptotic.boxTopError, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.boxSlackError, OAI.TotientAsymptotic.G