lintegral_exp_mul_sq_norm_le_mul — Mathlib

English

For IsProbabilityMeasure μ and annulus between two balls, the lintegral over the annulus of exp(logRatio · ‖x‖^2) is bounded by a linear combination of the integrals over inner regions and a bound involving logRatio and normThreshold.

Русский

Для IsProbabilityMeasure μ и кольца между двумя шарами линтеграл по кольцу от exp(logRatio · ‖x‖^2) ограничен линейной комбинацией интегралов по внутренним регионам и оценкой, зависящей от logRatio и normThreshold.

LaTeX

$$$\\int_{\\overline{B}_0(\\operatorname{normThreshold}(a,n+1))\\setminus\\overline{B}_0(\\operatorname{normThreshold}(a,n))} \\!\\exp\\big(\\logRatio(\\mu\\{\\|x\\|\\le a\\})\\;a^{-2}\\;\\|x\\|^{2}\\big) \, d\\mu(x) \\le \\mu\\{\\|x\\|\\le a\\} \\cdot \\exp( -2^{-1} \\log(\\tfrac{\\mu\\{\\|x\\|\\le a\\}}{1-\\mu\\{\\|x\\|\\le a\\}}) 2^{n} )$$

Lean4

theorem lintegral_exp_mul_sq_norm_le_mul [IsProbabilityMeasure μ]
    (h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ) (ha_pos : 0 < a) {c' : ℝ≥0∞}
    (hc' : c' ≤ μ {x | ‖x‖ ≤ a}) (hc'_gt : 2⁻¹ < c') :
    ∫⁻ x, .ofReal (rexp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
      μ {x | ‖x‖ ≤ a} *
        (.ofReal (rexp (logRatio c')) + ∑' n, .ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n))) :=
  by
  let t := normThreshold a
  let c := μ {x | ‖x‖ ≤ a}
  let C := logRatio c' * a⁻¹ ^ 2
  have hc'_le : c' ≤ 1 := hc'.trans prob_le_one
  change
    ∫⁻ x, .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
      c *
        (.ofReal (rexp (logRatio c')) + ∑' n, .ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))
          -- We will cut the space into a ball of radius `a` and annuli defined from the thresholds `t n`
            -- and bound the integral on each piece.
            -- First, we bound the integral on the ball of radius `a`

  have ht_int_zero :
    ∫⁻ x in closedBall 0 a, .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ μ {x | ‖x‖ ≤ a} * .ofReal (rexp (logRatio c')) := by
    calc
      ∫⁻ x in closedBall 0 a, .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
      _ ≤ ∫⁻ x in closedBall 0 a, .ofReal (rexp (C * a ^ 2)) ∂μ :=
        by
        refine setLIntegral_mono (by fun_prop) fun x hx ↦ ?_
        gcongr
        · exact mul_nonneg (logRatio_nonneg hc'_gt.le hc'_le) (by positivity)
        · simpa using hx
      _ = μ {x | ‖x‖ ≤ a} * .ofReal (rexp (logRatio c')) :=
        by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]
        rw [mul_comm]
        simp only [inv_pow, C]
        field_simp
        congr with x
        simp
          -- We dispense with an edge case. If `μ {x | ‖x‖ ≤ a} = 1`, then the integral over
            -- the complement of the ball is zero and we are done.

  by_cases ha : μ {x | ‖x‖ ≤ a} = 1
  · simp [c, ha] at ht_int_zero ⊢
    refine le_add_right ((le_of_eq ?_).trans ht_int_zero)
    rw [← setLIntegral_univ]
    refine setLIntegral_congr ?_
    rw [← ae_iff_prob_eq_one ?_] at ha
    · rw [eventuallyEq_comm, ae_eq_univ]
      change μ {x | ¬x ∈ closedBall 0 a} = 0
      rw [← ae_iff]
      filter_upwards [ha] with x hx using by simp [hx]
    · refine measurable_to_prop ?_
      rw [show (fun x : E ↦ ‖x‖ ≤ a) ⁻¹' { True } = {x : E | ‖x‖ ≤ a} by ext; simp]
      exact
        measurableSet_le (by fun_prop)
          (by fun_prop)
            -- So we can assume `μ {x | ‖x‖ ≤ a} < 1`, which implies `c' < 1`

  have ha_lt : μ {x | ‖x‖ ≤ a} < 1 := lt_of_le_of_ne prob_le_one ha
  have hc'_lt : c' < 1 := lt_of_le_of_lt hc' ha_lt
  have h_iUnion : (Set.univ : Set E) = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n) :=
    by
    ext x
    simp only [Set.mem_univ, Set.mem_union, Metric.mem_closedBall, dist_zero_right, Set.mem_iUnion, Set.mem_diff,
      not_le, true_iff]
    simp_rw [and_comm (b := t _ < ‖x‖)]
    rcases le_or_gt (‖x‖) a with ha' | ha'
    · exact Or.inl ha'
    ·
      exact
        Or.inr <|
          (normThreshold_strictMono ha_pos).exists_between_of_tendsto_atTop (tendsto_normThreshold_atTop ha_pos) ha'
  rw [← setLIntegral_univ, h_iUnion]
  have :
    ∫⁻ x in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n), .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
      ∫⁻ x in closedBall 0 (t 0), .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
        ∑' i, ∫⁻ x in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ :=
    by
    refine (lintegral_union_le _ _ _).trans ?_
    gcongr
    exact
      lintegral_iUnion_le _
        _
          -- Each of the integrals in the sum correspond to the terms in the goal

  refine this.trans ?_
  rw [mul_add]
  gcongr
    -- We already proved the upper bound for the ball

  · exact ht_int_zero
  rw [← ENNReal.tsum_mul_left]
  gcongr with n
  refine (le_trans ?_ (lintegral_closedBall_diff_exp_logRatio_mul_sq_le h_rot (hc'_gt.trans_le hc') ha_lt n)).trans ?_
  · gcongr
    simp only [inv_pow, C]
    field_simp
    exact logRatio_mono hc'_gt ha_lt hc'
  gcongr _ * ENNReal.ofReal (rexp ?_)
  simp only [ENNReal.toReal_div, neg_mul, neg_le_neg_iff]
  gcongr
  · refine div_pos ?_ ?_
    all_goals rw [ENNReal.toReal_pos_iff]
    · exact ⟨lt_trans (by norm_num) hc'_gt, by finiteness⟩
    · simp only [tsub_pos_iff_lt, hc'_lt, true_and]
      finiteness
  · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
    exact ⟨ha_lt, by finiteness⟩
  · finiteness
  · finiteness

Похожие утверждения