DeclHasVCDimLE.vcGrowth_le_exp
∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → d ≤ n → ↑(vcGrowth n 𝒜) ≤ (Real.exp 1 / ↑d * ↑n) ^ dArguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6002 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6002
Cite
Verification
- Library
- FLT_Proofs.VCDimGeneralized.VCDim
- Statement digest
- a5fe126e5cef
- First verified
- 2026-09-24T00:00:00Z