LeanMachineLearning exposition

ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le🔗

Minimal Lean file

measure_sum_le_sum_le🔗

LemmaProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le
Details

No docstring.

🔗theorem
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 ω => ∑ i ∈ s, X i ω) (fun ω => ∑ j ∈ t, Y j ω) μ)
  (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 ω => ∑ i ∈ s, X i ω)
      (fun ω => ∑ j ∈ t, Y j ω) μ)
  (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))))

Code

lemma measure_sum_le_sum_le [IsFiniteMeasure μ]
    (hX_indep : iIndepFun X μ) (hY_indep : iIndepFun Y μ)
    (hX_subG : ∀ i ∈ s, HasSubgaussianMGF (fun ω ↦ X i ω - μ[X i]) (cX i) μ)
    (hY_subG : ∀ j ∈ t, HasSubgaussianMGF (fun ω ↦ Y j ω - μ[Y j]) (cY j) μ)
    (h_indep_sum : IndepFun (fun ω ↦ ∑ i ∈ s, X i ω) (fun ω ↦ ∑ j ∈ t, Y j ω) μ)
    (h_le : ∑ j ∈ t, μ[Y j] ≤ ∑ i ∈ s, μ[X i]) :
    μ.real {ω | ∑ i ∈ s, X i ω ≤ ∑ j ∈ t, Y j ω}
      ≤ exp (- (∑ j ∈ t, μ[Y j] - ∑ i ∈ s, μ[X i]) ^ 2
        / (2 * (∑ i ∈ s, cX i + ∑ j ∈ t, cY j)))
Used by (1)

Actions: Source · Open Issue

Proof
by
  have hX_int i (his : i ∈ s) : Integrable (X i) μ := by
    have h_int := (hX_subG i his).integrable
    simp_rw [sub_eq_add_neg, integrable_add_const_iff] at h_int
    exact h_int
  have hY_int j (his : j ∈ t) : Integrable (Y j) μ := by
    have h_int := (hY_subG j his).integrable
    simp_rw [sub_eq_add_neg, integrable_add_const_iff] at h_int
    exact h_int
  refine (measureReal_le_le_exp
    (cX := ∑ i ∈ s, cX i) (cY := ∑ j ∈ t, cY j) ?_ ?_ h_indep_sum ?_).trans_eq ?_
  · suffices HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, (X i ω - μ[X i])) (∑ i ∈ s, cX i) μ by
      convert this
      rw [integral_finsetSum _ hX_int, Finset.sum_sub_distrib]
    refine sum_of_iIndepFun ?_ hX_subG
    exact hX_indep.comp (g := fun i x ↦ x - μ[X i]) (by fun_prop)
  · suffices HasSubgaussianMGF (fun ω ↦ ∑ j ∈ t, (Y j ω - μ[Y j])) (∑ j ∈ t, cY j) μ by
      convert this
      rw [integral_finsetSum _ hY_int, Finset.sum_sub_distrib]
    refine sum_of_iIndepFun ?_ hY_subG
    exact hY_indep.comp (g := fun i x ↦ x - μ[Y i]) (by fun_prop)
  · rwa [integral_finsetSum _ hX_int, integral_finsetSum _ hY_int]
  · congr
    · rw [integral_finsetSum _ hY_int]
    · rw [integral_finsetSum _ hX_int]