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
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞)
      (ENNReal.ofReal (rexp (logRatio c' * (HPow.hPow (β := ℕ) a 2)⁻¹ * HPow.hPow (β := ℕ) a 2))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
have field_simp : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c'))) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
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
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c'))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
have e_a : ∀ (x : E), Membership.mem (γ := Set E) (closedBall 0 a) x ↔ Membership.mem (γ := Set E) {x : E | ‖x‖ ≤ a} x
Tactic: congr with x
-- 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
⊢ ∫⁻ (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')))
have calc : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)) ∂μ
Tactic: 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
-- 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
calc :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)) ∂μ
⊢ ∫⁻ (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')))
have calc₁ : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)) ∂μ =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
Tactic: 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
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
⊢ ∫⁻ (x : E), 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 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')))
Tactic: 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
-- 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')))
⊢ ∫⁻ (x : E), 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 pos : ∀ (ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)),
  ∫⁻ (x : E), 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: by_cases ha : μ {x | ‖x‖ ≤ a} = 1
-- 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')))
pos :
  ∀ (ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)),
    ∫⁻ (x : E), 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), 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 : ∀ (ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)),
  ∫⁻ (x : E), 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: by_cases ha : μ {x | ‖x‖ ≤ a} = 1
-- 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∞)
⊢ ∫⁻ (x : E), 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 pos : ∀
  (ht_int_zero :
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
      ENNReal.ofReal (rexp (logRatio c'))),
  ∫⁻ (x : E), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c')) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c'.toReal / (1 - c').toReal) * HPow.hPow (α := ℝ) 2 n)))
Tactic: simp only [ha, one_mul, ENNReal.toReal_div, neg_mul, ge_iff_le, c] at ht_int_zero ⊢
Cleared hypotheses: ht_int_zero
-- 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
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c')) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c'.toReal / (1 - c').toReal) * HPow.hPow (α := ℝ) 2 n)))
have pos : ∫⁻ (x : E), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ =
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
Tactic: refine le_add_right ((le_of_eq ?_).trans ht_int_zero)
-- 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
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ =
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
have pos : ∫⁻ (x : E) in Set.univ, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ =
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
Tactic: rw [← setLIntegral_univ]
-- 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
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ ∫⁻ (x : E) in Set.univ, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ =
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
have pos : Set.univ =ᶠ[ae μ] closedBall 0 a
Tactic: refine setLIntegral_congr ?_
-- 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
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᶠ[ae μ] closedBall 0 a
have pos : ∀ (ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a)
  (ht_int_zero :
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
      ENNReal.ofReal (rexp (logRatio c'))),
  Set.univ =ᶠ[ae μ] closedBall 0 a
Tactic: rw [← ae_iff_prob_eq_one ?_] at ha
Cleared hypotheses: ha, ht_int_zero
-- 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
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
pos :
  ∀ (ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a)
    (ht_int_zero :
      ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
        ENNReal.ofReal (rexp (logRatio c'))),
    Set.univ =ᶠ[ae μ] closedBall 0 a
⊢ Set.univ =ᶠ[ae μ] closedBall 0 a
have rw : Measurable (β := Prop) fun (x : E) ↦ ‖x‖ ≤ a
Tactic: rw [← ae_iff_prob_eq_one ?_] at ha
-- 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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᶠ[ae μ] closedBall 0 a
have pos : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [eventuallyEq_comm, ae_eq_univ]
-- 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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | x ∉ closedBall 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ {x | ¬ x ∈ closedBall 0 a} = 0
-- 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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | x ∉ closedBall 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
have pos : ∀ᵐ (a_1 : E) ∂μ, Membership.mem (γ := Set E) (closedBall 0 a) a_1
Tactic: rw [← ae_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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
⊢ ∀ᵐ (a_1 : E) ∂μ, Membership.mem (γ := Set E) (closedBall 0 a) a_1
have h : ∀ (a_1 : E),
  Membership.mem (γ := Set E)
    {x : E |
      Membership.mem (γ := Set E) {x : E | (fun (a_2 : E) ↦ ‖a_2‖ ≤ a) x} x →
        Membership.mem (γ := Set E) {x : E | (fun (a_3 : E) ↦ Membership.mem (γ := Set E) (closedBall 0 a) a_3) x} x}
    a_1
Tactic: filter_upwards [ha] with x hx using by simp [hx]
-- 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
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c'))
h :
  ∀ (a_1 : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (a_2 : E) ↦ ‖a_2‖ ≤ a) x} x →
          Membership.mem (γ := Set E) {x : E | (fun (a_3 : E) ↦ Membership.mem (γ := Set E) (closedBall 0 a) a_3) x} x}
      a_1
⊢ ∀ᵐ (a_1 : E) ∂μ, Membership.mem (γ := Set E) (closedBall 0 a) a_1
have h₁ : ∀ (a_1 : E), ‖a_1‖ ≤ a → Membership.mem (γ := Set E) (closedBall 0 a) a_1
Tactic: filter_upwards [ha] with x hx using by simp [hx]