awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
⊢ ∫⁻ (a : E) in ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 2)) ∂μ ≤
    ∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ

Tactic:
exact lintegral_iUnion_le _ _

Premises used: MeasureTheory.lintegral_iUnion_le
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
⊢ ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ

Tactic:
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 _ _
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
⊢ ∫⁻ (x : E) in closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))

Tactic:
this.trans ?_

Premises used: ProbabilityTheory.Fernique.normThreshold, LE.le.trans, arithGeom
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
neg :
  ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
⊢ ∫⁻ (x : E) in closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
neg :
  ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (logRatio c')) +
      c * ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
neg :
  ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (logRatio c'))
neg₁ :
  ∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (logRatio c')) +
      c * ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
⊢ ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
ht_int_zero

Premises used: ProbabilityTheory.Fernique.normThreshold, arithGeom
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
⊢ ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
exact ht_int_zero
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
neg :
  LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ)
    (∑' (i : ℕ), c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 i)))
⊢ ∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
rw [← ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
neg :
  ∀ (n : ℕ),
    ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
      c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ LE.le (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ)
    (∑' (i : ℕ), c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 i)))

Tactic:
gcongr with n
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
      ∑' (i : ℕ),
        ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
n : ℕ
⊢ ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
(le_trans ?_ (lintegral_closedBall_diff_exp_logRatio_mul_sq_le h_rot
    (hc'_gt.trans_le hc') ha_lt n)).trans ?_

Premises used: ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le, LT.lt.trans_le, LE.le.trans, le_trans