AffineUniformCertificate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.FullCertificate.uniform_activity line 14
Source documentation
A fixed full affine certificate gives a uniform activity bound on its exponent cube at all sufficiently small positive scales.
```
theorem FullCertificate.uniform_activity {d : ℕ} {a b : ℝ}
    {E : (Fin d → ℝ) → ℝ} (C : FullCertificate d a b E) :
    ∃ h0 : ℝ, 0 < h0 ∧ ∀ h : ℝ, 0 < h → h < h0 →
      ∀ p : Fin d → ℝ, Cube a b p → ∀ L ∈ C.labels,
        Active C.labels L h (powerPoint h p) → ‖p - L.slope‖ < E L.slope := by
…
```
Mentions: OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint