∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α}, ((fun x => A ∩ x) '' 𝒜).encard ≤ {B | B ⊆ A ∧ Shatters 𝒜 B}.encard

∀ {α : Type u_1} {n d : ℕ} {𝒜 : Set (Set α)}, HasVCDimLE d 𝒜 → d ≤ n → ↑(vcGrowth n 𝒜) ≤ (Real.exp 1 / ↑d * ↑n) ^ d

∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
  Cardinal.mk ↑{t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t} ≤
    Cardinal.mk ↑{B | B ⊆ A ∧ Shatters 𝒜 B}

¬Cardinal.mk ↑((fun x => Set.univ ∩ x) '' Set.range fun r => {q | ↑q < r}) ≤
    Cardinal.mk ↑{B | B ⊆ Set.univ ∧ Shatters (Set.range fun r => {q | ↑q < r}) B}

∀ {X : Type u_1} {Y : Type u_2} (𝒞 : Set (X → Y)) (S : Set X), (S.restrict '' 𝒞).encard ≤ (pairCubes 𝒞 S).encard

∃ 𝒞, HasNatarajanDimLE 1 𝒞 ∧ ¬HasDSDimLE 1 𝒞

∀ {α : Type u} {𝒜 : Set (Set α)} {A : Set α} {d : ℕ},
  HasVCDimLE d 𝒜 → A.Infinite → Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) ≤ ded (Cardinal.mk ↑A)

∀ {κ : Cardinal.{u}},
  Cardinal.aleph0 ≤ κ →
    ∀ {lam : Cardinal.{u}},
      lam < ded κ → ∃ α 𝒜 A, Cardinal.mk ↑A = κ ∧ HasVCDimLE 1 𝒜 ∧ lam < Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜)

∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k

∀ (X : Type) (C : ConceptClass X Bool), OnlineLearnable X Bool C ↔ LittlestoneDim X C < ⊤

∀ (X : Type) (C : ConceptClass X Bool), Set.Nonempty C → ↑(OptimalMistakeBound X C) = LittlestoneDim X C

∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C],
  (∀ (L : BatchLearner X Bool), LearnEvalMeasurable L) → UniversalLearnable X C → PACLearnable X C

KrappWirthSeparationMeasTarget

∀ (d : ℕ),
  ¬∃ t,
      KWLock.Realizes (KWLock.onesOf (KWLock.Fd 4 KWLock.fA (d + 1))) (KWLock.zerosOf (KWLock.Fd 4 KWLock.fA (d + 1)))
        (KWLock.towerP 4 KWLock.fA KWLock.pA d) t

∀ {Ωtrain : Type u_1} {Z : Type u_2} {ι : Type u_3} [inst : MeasurableSpace Ωtrain] [inst_1 : MeasurableSpace Z]
  [inst_2 : Fintype ι] [Nonempty ι] (μtrain : AuditCP.AuditSampleLaw Ωtrain) [MeasureTheory.IsProbabilityMeasure μtrain]
  (Q : AuditCP.AuditSampleLaw Z) [MeasureTheory.IsProbabilityMeasure Q] (n : ℕ),
  0 < n →
    ∀ (a b : ℝ),
      a < b →
        ∀ (δ : ℝ),
          0 < δ →
            δ ≤ 1 →
              ∀ (loss : ι → Z → ℝ),
                (∀ (i : ι), Measurable (loss i)) →
                  (∀ (i : ι), ∀ᵐ (z : Z) ∂Q, loss i z ∈ Set.Icc a b) →
                    ∀ (F : Ωtrain → AuditCP.AuditEnvelope ι) (g : Ωtrain → AuditCP.AuditTrajectory ι),
                      (∀ (t : Ωtrain), AuditCP.Admissible (g t) (F t)) →
                        MeasurableSet
                            {p |
                              ¬AuditCP.UniformDev (F p.1) (fun i => AuditCP.empiricalLoss loss i p.2)
                                  (fun i => AuditCP.populationLoss Q loss i)
                                  (AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ)} →
                          ∀ (T : ℕ),
                            (MeasureTheory.Measure.prod μtrain (MeasureTheory.Measure.pi fun x => Q))
                                {p |
                                  AuditCP.cumCP (fun i => AuditCP.empiricalLoss loss i p.2) (g p.1) T >
                                    AuditCP.cumCP (fun i => AuditCP.populationLoss Q loss i) (g p.1) T +
                                      2 * AuditCP.deltaFiniteExperts (Fintype.card ι) n (b - a) δ} ≤
                              ENNReal.ofReal δ

∀ {S : Type uS} {A : Type uA} {Y : Type uY} [Nonempty A] (K : AuditCP.AuditChannel S A Y),
  AuditCP.BlackwellEquivalent (AuditCP.learnerExperiment K) AuditCP.publicOnlyExperiment ↔ AuditCP.AuditSealed K

∀ {S : Type uS} {A : Type uA} {Y : Type uY} [inst : Fintype Y] (K : AuditCP.AuditChannel S A Y),
  AuditCP.AuditSealed K ↔ ∀ (s : S) (a a' : A), AuditCP.equalPriorBayesError (K (s, a)) (K (s, a')) = 1 / 2

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α]
  {cap : Set α → ENNReal},
  MeasureTheory.IsChoquetCapacity cap →
    ∀ {s : Set α}, MeasureTheory.AnalyticSet s → cap s = ⨆ K, ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap K

∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (𝒞 : Finset (Finset ι)),
  HiddenChannelCapacity.Acyclic 𝒞 ↔
    ∀ (fam : List (HiddenChannelCapacity.LocalStruct ι fun x => ZMod 2)),
      List.map (fun x => x.team) fam = 𝒞.toList →
        HiddenChannelCapacity.Consistent fam → (∀ L ∈ fam, L.rel.Nonempty) → HiddenChannelCapacity.Glues fam

∀ {ι : Type u_1} [inst : DecidableEq ι] (𝒞 : Finset (Finset ι)),
  (¬∃ l, HiddenChannelCapacity.IsChordlessCycle 𝒞 l) →
    ∀ (S : Finset ι),
      (∀ x ∈ S, ∀ y ∈ S, x ≠ y → HiddenChannelCapacity.Adj 𝒞 x y) ∨
        ∃ u w,
          HiddenChannelCapacity.SimpIn 𝒞 S u ∧
            HiddenChannelCapacity.SimpIn 𝒞 S w ∧ u ≠ w ∧ ¬HiddenChannelCapacity.Adj 𝒞 u w

∀ {a : Type u_1} {c : Type u_2} {b : Type u_3} [inst : Fintype a] [inst_1 : DecidableEq a] [inst_2 : Nonempty a]
  [inst_3 : Fintype c] [inst_4 : DecidableEq c] [inst_5 : Nonempty c] [inst_6 : Fintype b] [inst_7 : DecidableEq b]
  [inst_8 : Nonempty b] {ρAC : MState (a × c)} {ρCB : MState (c × b)},
  ρAC.m.PosDef →
    ρCB.m.PosDef →
      ρAC.traceLeft = ρCB.traceRight →
        (HiddenChannelCapacity.trC ρAC ρCB = 1 ↔ ∃ ω, HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω) ∧
          ∀ (ω : MState (a × c × b)),
            HiddenChannelCapacity.IsMarkovCompletion ρAC ρCB ω → ω = HiddenChannelCapacity.sigT ρAC ρCB

∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m₁ m₂ : EuclideanSpace ℝ ι) {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef →
    S₂.PosDef →
      InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian m₁ S₁)
          (ProbabilityTheory.multivariateGaussian m₂ S₂) =
        1 / 2 *
          (Real.log (S₂.det / S₁.det) + (S₂⁻¹ * S₁).trace + (m₁ - m₂).ofLp ⬝ᵥ S₂⁻¹.mulVec (m₁.ofLp - m₂.ofLp) -
            ↑(Fintype.card ι))

∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A

∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α)
  [inst_1 : MeasureTheory.IsProbabilityMeasure P] [inst_2 : MeasureTheory.IsProbabilityMeasure Q],
  P.AbsolutelyContinuous Q →
    MeasureTheory.Integrable (MeasureTheory.llr P Q) P →
      MeasureTheory.tvDistReal P Q ≤ √(InformationTheory.klDivReal P Q / 2)

∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Set α)},
  StructuralIgnorance.vcBounded 𝒜 1 → StructuralIgnorance.HasKernelScheme 𝒜 1

∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool)
  [MeasurableConceptClass X C],
  (PACLearnable X C ↔ VCDim X C < ⊤) ∧
    (VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k) ∧
      (VCDim X C < ⊤ ↔
          ∀ ε > 0,
            ∃ m₀,
              ∀ (D : MeasureTheory.Measure X),
                MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) ∧
        (PACLearnable X C →
            ∃ L mf,
              (∀ (ε δ : ℝ),
                  0 < ε →
                    0 < δ →
                      ∀ (D : MeasureTheory.Measure X),
                        MeasureTheory.IsProbabilityMeasure D →
                          ∀ c ∈ C,
                            (MeasureTheory.Measure.pi fun x => D)
                                {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥
                              ENNReal.ofReal (1 - δ)) ∧
                (∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ) ∧
                  ∀ (d : ℕ),
                    VCDim X C = ↑d →
                      ∀ (ε δ : ℝ),
                        0 < ε →
                          ε ≤ 1 / 4 →
                            0 < δ →
                              δ ≤ 1 →
                                δ ≤ 1 / 7 →
                                  1 ≤ d → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ ∧ ⌈(↑d - 1) / 2⌉₊ ≤ mf ε δ) ∧
          (VCDim X C < ⊤ ↔ ∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i)

∀ {X : Type u} [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool)
  [MeasurableConceptClass X C],
  (VCDim X C < ⊤ ↔ PACLearnable X C) ∧
    (VCDim X C < ⊤ ↔ ∃ K d, ∀ᶠ (m : ℕ) in Filter.atTop, ↑(GrowthFunction X C m) ≤ K * ↑m ^ d)

(∀ (X : Type) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableConceptClass X C],
    OnlineLearnable X Bool C → PACLearnable X C) ∧
  ∃ X x C, PACLearnable X C ∧ ¬OnlineLearnable X Bool C

∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C] (A : Type u_1)
  [inst_2 : Fintype A] [inst_3 : Nonempty A], PACLearnableWithAdviceRegular X C A → PACLearnable X C

∀ (n : ℕ), VCDim (Fin n → ℝ) (signClass (FLT.Halfspace.coordSpace n)) = ↑n

∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C ≤ ↑d → VCDim (↑C) (dualClass C) ≤ ↑(2 ^ (d + 1) - 1)

∀ {X : Type u} {C : ConceptClass X Bool} {d : ℕ}, VCDim X C = ↑d → 0 < d → ↑(Nat.log 2 d) ≤ VCDim (↑C) (dualClass C)

(n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) n