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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ (b - a) / √2 < min ‖p.1‖ ‖p.2‖
have calc : (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
Tactic: calc (b - a) / √2
    _ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
      suffices b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 by
        calc (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 := by gcongr
        _ = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
          field_simp; rw [Real.sq_sqrt (by positivity)]; ring
      calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
    _ ≤ min ‖p.1‖ ‖p.2‖ := by
      have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
calc : (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
⊢ (b - a) / √2 < min ‖p.1‖ ‖p.2‖
have calc₁ : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
Tactic: calc (b - a) / √2
    _ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
      suffices b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 by
        calc (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 := by gcongr
        _ = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
          field_simp; rw [Real.sq_sqrt (by positivity)]; ring
      calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
    _ ≤ min ‖p.1‖ ‖p.2‖ := by
      have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
      (SProd.sprod (α := Set E) (β := Set E) {x : E | (b - a) / √2 < ‖x‖} {y : E | (b - a) / √2 < ‖y‖}) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞) ≤
  HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
Tactic: rw [Measure.prod_prod, pow_two]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
⊢ (μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
      (SProd.sprod (α := Set E) (β := Set E) {x : E | (b - a) / √2 < ‖x‖} {y : E | (b - a) / √2 < ‖y‖}) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞)
Tactic: rw [Measure.prod_prod, pow_two]
-- 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
inst_5 : SFinite μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
n : ℕ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
have h : ∀ (x : E), normThreshold a n = (normThreshold a (n + 1) - a) / √2
Tactic: convert! measure_le_mul_measure_gt_le_of_map_rotation_eq_self h_rot _ _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
ha_pos : 0 < a
⊢ a / (1 - √2) < normThreshold a 0
have simp : a / (1 - √2) < a
Tactic: simp only [normThreshold_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ normThreshold a n = a * (1 + √2) * (√2 ^ (n + 1) - 1)
have rw : a * (√2 ^ (n + 1) - 1) * (√2 + 1) = a * (1 + √2) * (√2 ^ (n + 1) - 1)
Tactic: rw [normThreshold, arithGeom_same_eq_mul_div (by simp), div_eq_mul_inv, Real.inv_sqrt_two_sub_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
    HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)
have simp_rw : HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2) ≤
  HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2))
Tactic: simp_rw [normThreshold_eq, mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2) ≤
    HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2))
have hbc : HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2 ≤ HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2
have ha : 0 ≤ √2 ^ (n + 2) - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
ha : 0 ≤ √2 ^ (n + 2) - 1
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2
have hab : √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1 ≤ √2 ^ (n + 2) - 1
have h : 1 ≤ √2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
h : 1 ≤ √2
⊢ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1 ≤ √2 ^ (n + 2) - 1
have h₁ : 0 ≤ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ 0 ≤ √2 ^ (n + 2) - 1
have calc : 0 ≤ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1
Tactic: calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
calc : 0 ≤ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1
⊢ 0 ≤ √2 ^ (n + 2) - 1
have calc₁ : √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1 ≤ √2 ^ (n + 2) - 1
Tactic: calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
have rw : √2 ^ ((n + 2) * 2) = HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
rw : √2 ^ ((n + 2) * 2) = HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
have rw₁ : √2 ^ (2 * (n + 2)) = HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
rw : √2 ^ ((n + 2) * 2) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₁ : √2 ^ (2 * (n + 2)) = HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
have rw₂ : HPow.hPow (β := ℕ) (√2) 2 ^ (n + 2) = HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
rw : √2 ^ ((n + 2) * 2) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₁ : √2 ^ (2 * (n + 2)) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₂ : HPow.hPow (β := ℕ) (√2) 2 ^ (n + 2) = HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
have rw₃ : HPow.hPow (α := ℝ) 2 (n + 2) = HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2 ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have calc : HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2
Tactic: calc (√2 ^ (n + 2) - 1) ^ 2
  _ ≤ (√2 ^ (n + 2)) ^ 2 := by
    gcongr
    · calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
    · exact sub_le_self _ (by simp)
  _ = 2 ^ (n + 2) := by rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
n : ℕ
calc : HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2 ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have calc₁ : HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: calc (√2 ^ (n + 2) - 1) ^ 2
  _ ≤ (√2 ^ (n + 2)) ^ 2 := by
    gcongr
    · calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
    · exact sub_le_self _ (by simp)
  _ = 2 ^ (n + 2) := by rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]
-- 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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
have hc_pos : 0 < c
Tactic: have hc_pos : 0 < c := lt_of_lt_of_le (by simp) hc_gt.le
-- 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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
have hc_lt_top : c < ∞
Tactic: have hc_lt_top : c < ∞ := measure_lt_top _ _
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a 0 < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) (β := ℕ) 2 0)
have zero : (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
    (HDiv.hDiv (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
Tactic: simp only [pow_zero, pow_one, normThreshold_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_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
        (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
        ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
have zero : (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
Tactic: rw [ENNReal.mul_div_cancel hc_pos.ne' hc_lt_top.ne]
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
have zero : (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
Tactic: refine le_of_eq ?_
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ Measurable.{u_1, 0} (α := E) norm
have funProp : inst_3 ≤ inst_3
Tactic: fun_prop
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
funProp : inst_3 ≤ inst_3
⊢ Measurable.{u_1, 0} (α := E) norm
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : E) ↦ ‖a‖
Tactic: fun_prop
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
have zero : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) {a_1 : E | ‖a_1‖ ≤ a}ᶜ : ℝ≥0∞)
Tactic: rw [← prob_compl_eq_one_sub (measurableSet_le (by fun_prop) (by fun_prop))]
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {a_1 : E | ‖a_1‖ ≤ a}ᶜ : ℝ≥0∞)
have zero : ∀ (x : E), a < ‖x‖ ↔ x ∉ {a_1 : E | ‖a_1‖ ≤ a}
Tactic: congr with x
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 (n + 1))
have h_mul_le : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
  HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
Tactic: have h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖}
        ≤ μ {x | normThreshold a n < ‖x‖} ^ 2 :=
      measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self h_rot _ _
-- 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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
    c⁻¹ * HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
have rw : (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
  HMul.hMul (β := ℝ≥0∞) (c⁻¹ * c) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]