awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)) ∂μ +
      ∑' (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)))
have 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))
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)) ∂μ +
      ∑' (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))
have neg : ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
  c * ENNReal.ofReal (rexp (logRatio c'))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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'))
⊢ ∫⁻ (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))
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)) ∂μ
⊢ ∑' (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))
have 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)))
Tactic: rw [← ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)) ∂μ
⊢ 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)))
have 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))
Tactic: gcongr with n
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (normThreshold a (n + 1)) \ closedBall 0 (normThreshold a n),
      ENNReal.ofReal
        (rexp
          (logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) a⁻¹ 2 *
            HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
have neg : ∀ (x : E), C ≤ logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) a⁻¹ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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
⊢ C ≤ logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) a⁻¹ 2
have neg : logRatio c' * (HPow.hPow (β := ℕ) a 2)⁻¹ ≤
  logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * (HPow.hPow (β := ℕ) a 2)⁻¹
Tactic: simp only [inv_pow, C]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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
⊢ logRatio c' * (HPow.hPow (β := ℕ) a 2)⁻¹ ≤
    logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * (HPow.hPow (β := ℕ) a 2)⁻¹
have neg : logRatio c' ≤ logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a})
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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 : ℕ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-2⁻¹ *
              Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n))) ≤
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n))
have neg : -2⁻¹ *
      Real.log
        (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
            (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
    HPow.hPow (α := ℝ) 2 n ≤
  -2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n
Tactic: gcongr _ * ENNReal.ofReal (rexp ?_)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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 : ℕ
⊢ -2⁻¹ *
        Real.log
          (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
              (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
      HPow.hPow (α := ℝ) 2 n ≤
    -2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n
have neg : 2⁻¹ * Real.log (c'.toReal / (1 - c').toReal) * HPow.hPow (α := ℝ) 2 n ≤
  2⁻¹ *
      Real.log
        (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) /
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)).toReal) *
    HPow.hPow (α := ℝ) 2 n
Tactic: simp only [ENNReal.toReal_div, neg_mul, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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 : ℕ
⊢ 2⁻¹ * Real.log (c'.toReal / (1 - c').toReal) * HPow.hPow (α := ℝ) 2 n ≤
    2⁻¹ *
        Real.log
          (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) /
            (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)).toReal) *
      HPow.hPow (α := ℝ) 2 n
have neg : 0 < c'.toReal / (1 - c').toReal
Tactic: gcongr