ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'.{u_1, u_2,
    u_3}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι : Type u_2} {ι' : Type u_3} {X : ι → Ω → ℝ} {cX : ι → NNReal}
  {s : Finset ι} {Y : ι' → Ω → ℝ} {cY : ι' → NNReal} {t : Finset ι'}
  [MeasureTheory.IsFiniteMeasure μ] (hX_indep : iIndepFun X μ)
  (hY_indep : iIndepFun Y μ)
  (hX_subG :
    ∀ i ∈ s,
      HasSubgaussianMGF (fun ω => X i ω - ∫ (x : Ω), X i x ∂μ) (cX i) μ)
  (hY_subG :
    ∀ j ∈ t,
      HasSubgaussianMGF (fun ω => Y j ω - ∫ (x : Ω), Y j x ∂μ) (cY j) μ)
  (h_indep_sum : IndepFun (fun ω x => X x ω) (fun ω x => Y x ω) μ)
  (h_le : ∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ ≤ ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) :
  MeasureTheory.Measure.real μ {ω | ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω} ≤
    Real.exp
      (-(∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ - ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) ^
            2 /
        (2 * (↑(∑ i ∈ s, cX i) + ↑(∑ j ∈ t, cY j))))
ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'.{u_1,
    u_2, u_3}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω}
  {ι : Type u_2} {ι' : Type u_3}
  {X : ι → Ω → ℝ} {cX : ι → NNReal}
  {s : Finset ι} {Y : ι' → Ω → ℝ}
  {cY : ι' → NNReal} {t : Finset ι'}
  [MeasureTheory.IsFiniteMeasure μ]
  (hX_indep : iIndepFun X μ)
  (hY_indep : iIndepFun Y μ)
  (hX_subG :
    ∀ i ∈ s,
      HasSubgaussianMGF
        (fun ω =>
          X i ω - ∫ (x : Ω), X i x ∂μ)
        (cX i) μ)
  (hY_subG :
    ∀ j ∈ t,
      HasSubgaussianMGF
        (fun ω =>
          Y j ω - ∫ (x : Ω), Y j x ∂μ)
        (cY j) μ)
  (h_indep_sum :
    IndepFun (fun ω x => X x ω)
      (fun ω x => Y x ω) μ)
  (h_le :
    ∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ ≤
      ∑ i ∈ s, ∫ (x : Ω), X i x ∂μ) :
  MeasureTheory.Measure.real μ
      {ω |
        ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω} ≤
    Real.exp
      (-(∑ j ∈ t, ∫ (x : Ω), Y j x ∂μ -
              ∑ i ∈ s,
                ∫ (x : Ω), X i x ∂μ) ^
            2 /
        (2 *
          (↑(∑ i ∈ s, cX i) +
            ↑(∑ j ∈ t, cY j))))