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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ ∫⁻ (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 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) ∂μ
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x),
  ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2))
Tactic: refine setLIntegral_mono (by fun_prop) fun x 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2))
have h : 0 ≤ 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x
h : 0 ≤ C
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2))
have h₁ : ‖x‖ ≤ t (n + 1)
Tactic: gcongr
-- 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x
⊢ ‖x‖ ≤ t (n + 1)
have hx₁ : ‖x‖ ≤ t (n + 1) ∧ t n < ‖x‖
Tactic: simp only [Set.mem_diff, mem_closedBall, dist_zero_right, not_le] at hx
Cleared hypotheses: 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)))
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)))
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} : ℝ≥0∞)
have bc : Subset.{u_1} (α := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) {x : E | t n < ‖x‖}
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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
| ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) * c *
    ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
have rw : ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) *
  (c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))
Tactic: rw [mul_assoc]
-- 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)))
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} : ℝ≥0∞) ≤
    ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
have conv_rhs : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)))
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} : ℝ≥0∞) ≤
  ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) *
    (c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))
Tactic: conv_rhs => rw [mul_assoc]
-- 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)))
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} : ℝ≥0∞) ≤
    ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) *
      (c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))
have bc : (μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} ≤
  c * ENNReal.ofReal (rexp (-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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) ≤
    ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
have bc : C * HPow.hPow (β := ℕ) (t (n + 1)) 2 ≤ 2⁻¹ * Real.log (c.toReal / (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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ C * HPow.hPow (β := ℕ) (t (n + 1)) 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
have h : C * HPow.hPow (β := ℕ) (t (n + 1)) 2 =
  logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 *
    HPow.hPow (β := ℕ) a⁻¹ 2
Tactic: convert! logRatio_mul_normThreshold_add_one_le ha_gt ha_lt n (a := a) using 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
have rw : c *
    ENNReal.ofReal
      (rexp
        (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
          -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
  c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
Tactic: rw [mul_comm _ c, mul_assoc, ← ENNReal.ofReal_mul (by positivity), ← Real.exp_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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ c *
      ENNReal.ofReal
        (rexp
          (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
            -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
have e_a : 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
    -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n =
  -2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n
Tactic: 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
      -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n
have e_a : 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) +
    -Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) =
  -2⁻¹ * Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ)
Tactic: norm_cast
-- 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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) +
      -Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ)
have e_a : 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
    -Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n =
  -2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
Tactic: simp only [Nat.cast_pow, Nat.cast_ofNat, ENNReal.toReal_div]
-- 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
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
have hc'_le : c' ≤ 1
Tactic: have hc'_le : c' ≤ 1 := hc'.trans prob_le_one
-- 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)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)) ∂μ
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) (closedBall 0 a) x),
  ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))
Tactic: refine setLIntegral_mono (by fun_prop) fun x 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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) x
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))
have h : 0 ≤ 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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) x
h : 0 ≤ C
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))
have h₁ : ‖x‖ ≤ a
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
⊢ ∫⁻ (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')))
have simp : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)))
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
Tactic: simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]
-- 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∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)))
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
have rw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞)
    (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: rw [mul_comm]
-- 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 (C * HPow.hPow (β := ℕ) a 2))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
have simp : 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')))
Tactic: simp only [inv_pow, C]