def WellBehavedVCMeasTarget
    (X : Type u) [MeasurableSpace X]
    (C : ConceptClass X Bool) : Prop :=
  forall (D : Measure X) [IsProbabilityMeasure D]
    (c : Concept X Bool), Measurable c ->
    forall (m : N) (e : R),
      NullMeasurableSet
        {p : (Fin m -> X) * (Fin m -> X) | exists h (*@$\in$@*) C,
          EmpiricalError X Bool h
            (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) -
          EmpiricalError X Bool h
            (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) (*@$\geq$@*) e / 2}
        ((Measure.pi (fun _ : Fin m => D)).prod
         (Measure.pi (fun _ : Fin m => D)))

class KrappWirthWellBehaved (X : Type u) [MeasurableSpace X]
    (C : ConceptClass X Bool) : Prop extends MeasurableHypotheses X C where
  V_measurable : KrappWirthV X C
  U_measurable : KrappWirthU X C

theorem singleton_badEvent_not_measurable
    (A : Set R) (hA_non : (*@$\neg$@*) MeasurableSet A) :
    (*@$\neg$@*) MeasurableSet (singletonBadEvent A) := by
  intro hbad
  rw [singleton_badEvent_eq_preimage_planar A] at hbad
  have hmeas : Measurable samplePair1ToPlane :=
    Measurable.prod
      ((measurable_pi_apply 0).comp measurable_fst)
      ((measurable_pi_apply 0).comp measurable_snd)
  have hsurj : Function.Surjective samplePair1ToPlane := by
    intro (*@$\langle$@*)x, y(*@$\rangle$@*)
    exact (*@$\langle$@*)(fun _ => x, fun _ => y), by simp [samplePair1ToPlane](*@$\rangle$@*)
  have hplanar :=
    (hmeas.measurableSet_preimage_iff_of_surjective hsurj).mp hbad
  exact planarWitnessEvent_not_measurable A hA_non hplanar

theorem analyticSet_nullMeasurableSet
    {(*@$\alpha$@*) : Type*}
    [TopologicalSpace (*@$\alpha$@*)] [MeasurableSpace (*@$\alpha$@*)]
    [BorelSpace (*@$\alpha$@*)] [PolishSpace (*@$\alpha$@*)]
    {(*@$\mu$@*) : Measure (*@$\alpha$@*)} [IsFiniteMeasure (*@$\mu$@*)]
    {s : Set (*@$\alpha$@*)} (hs : AnalyticSet s) :
    NullMeasurableSet s (*@$\mu$@*) := by
  classical
  obtain (*@$\langle$@*)t, hst, ht_meas, ht_eq(*@$\rangle$@*) :=
    exists_measurable_superset (*@$\mu$@*) s
  have hzero : (*@$\mu$@*) (t \ s) = 0 := by
    by_contra hne
    have hfin_diff : (*@$\mu$@*) (t \ s) (*@$\neq$@*) (*@$\top$@*) := measure_ne_top (*@$\mu$@*) _
    have hpos : 0 < (*@$\mu$@*).real (t \ s) :=
      ENNReal.toReal_pos hne hfin_diff
    obtain (*@$\langle$@*)K, hKc, hKs, hKapprox(*@$\rangle$@*) :=
      hs.exists_isCompact_measureReal_gt
        ((*@$\mu$@*) := (*@$\mu$@*)) ((*@$\mu$@*).real (t \ s) / 2) (by positivity)
    have hKt : K (*@$\subseteq$@*) t := fun x hx => hst (hKs hx)
    have hKmeas : MeasurableSet K := hKc.isClosed.measurableSet
    have hdiff_eq : (*@$\mu$@*).real (t \ K) = (*@$\mu$@*).real t - (*@$\mu$@*).real K :=
      measureReal_diff hKt hKmeas
    have ht_real : (*@$\mu$@*).real t = (*@$\mu$@*).real s := by
      simp only [Measure.real]; rw [ht_eq]
    have hsub : t \ s (*@$\subseteq$@*) t \ K :=
      Set.diff_subset_diff_right hKs
    have hle : (*@$\mu$@*).real (t \ s) (*@$\leq$@*) (*@$\mu$@*).real (t \ K) :=
      measureReal_mono hsub
    linarith
  have h_ae : s =(*@${}^{\text{ae}}$@*)[(*@$\mu$@*)] t := by
    rw [Filter.eventuallyEq_comm, ae_eq_set]
    exact (*@$\langle$@*)hzero, by simp [Set.diff_eq_empty.mpr hst](*@$\rangle$@*)
  exact ht_meas.nullMeasurableSet.congr h_ae.symm