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
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'))
⊢ Measurable (β := Prop) fun (x : E) ↦ ‖x‖ ≤ a
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_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'))
funProp : inst_3 ≤ inst_3
⊢ Measurable (β := Prop) fun (x : E) ↦ ‖x‖ ≤ a
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : E) ↦ ‖a‖
Tactic: fun_prop
-- 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
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 ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: have ha_lt : μ {x | ‖x‖ ≤ a} < 1 := lt_of_le_of_ne prob_le_one ha
-- 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
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∞)
⊢ ∫⁻ (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 hc'_lt : c' < 1
Tactic: have hc'_lt : c' < 1 := lt_of_le_of_lt hc' ha_lt
-- 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
⊢ Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
have h : ∀ (x : E),
  Membership.mem (γ := Set E) Set.univ x ↔
    Membership.mem (γ := Set E) (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x
Tactic: ext 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
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
x : E
⊢ Membership.mem (γ := Set E) Set.univ x ↔
    Membership.mem (γ := Set E) (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x
have h : ‖x‖ ≤ a ∨ ∃ (i : ℕ), ‖x‖ ≤ t (i + 1) ∧ t i < ‖x‖
Tactic: simp only [Set.mem_univ, Set.mem_union, Metric.mem_closedBall, dist_zero_right, Set.mem_iUnion,
      Set.mem_diff, not_le, true_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
x : E
⊢ ‖x‖ ≤ a ∨ ∃ (i : ℕ), ‖x‖ ≤ t (i + 1) ∧ t i < ‖x‖
have h : ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
Tactic: simp_rw [and_comm (b := t _ < ‖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
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
x : E
⊢ ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
have h : ∀ (ha' : ‖x‖ ≤ a), ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
Tactic: rcases le_or_gt (‖x‖) a with ha' | 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
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
x : E
h : ∀ (ha' : ‖x‖ ≤ a), ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
⊢ ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
have h₁ : ∀ (ha' : a < ‖x‖), ‖x‖ ≤ a ∨ ∃ (i : ℕ), t i < ‖x‖ ∧ ‖x‖ ≤ t (i + 1)
Tactic: rcases le_or_gt (‖x‖) a with ha' | ha'
-- 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
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
⊢ ∫⁻ (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 h_iUnion : Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
Tactic: have h_iUnion : (Set.univ : Set E)
      = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n) := by
    ext x
    simp only [Set.mem_univ, Set.mem_union, Metric.mem_closedBall, dist_zero_right, Set.mem_iUnion,
      Set.mem_diff, not_le, true_iff]
    simp_rw [and_comm (b := t _ < ‖x‖)]
    rcases le_or_gt (‖x‖) a with ha' | ha'
    · exact Or.inl ha'
    · exact Or.inr <| (normThreshold_strictMono ha_pos).exists_between_of_tendsto_atTop
        (tendsto_normThreshold_atTop ha_pos) 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
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
⊢ ∫⁻ (x : E), 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 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
    ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
  c *
    (ENNReal.ofReal (rexp (logRatio c')) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
Tactic: rw [← setLIntegral_univ, h_iUnion]
-- 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))
⊢ ∫⁻ (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)) ∂μ
have refine : ∫⁻ (a : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 2)) ∂μ +
    ∫⁻ (a : E) in ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 2)) ∂μ ≤
  ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ +
    ∑' (i : ℕ),
      ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
Tactic: refine (lintegral_union_le _ _ _).trans ?_
-- 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))
⊢ ∫⁻ (a : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 2)) ∂μ +
      ∫⁻ (a : E) in ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
        ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 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)) ∂μ
have bc : ∫⁻ (a : E) in ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
    ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖a‖ 2)) ∂μ ≤
  ∑' (i : ℕ),
    ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ
Tactic: 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_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
C : ℝ := logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
ha : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
hc'_lt : c' < 1
h_iUnion :
  Eq.{u_1 + 1} (α := Set E) Set.univ (closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n))
⊢ ∫⁻ (x : E) in closedBall 0 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
have 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)) ∂μ
Tactic: have : ∫⁻ x in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
        .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
      ≤ ∫⁻ x in closedBall 0 (t 0), .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
        ∑' i, ∫⁻ x in closedBall 0 (t (i + 1)) \ closedBall 0 (t i),
          .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ := by
    refine (lintegral_union_le _ _ _).trans ?_
    gcongr
    exact lintegral_iUnion_le _ _
-- 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 a ∪ ⋃ (n : ℕ), closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    c *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
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')) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * HPow.hPow (α := ℝ) 2 n)))
Tactic: refine this.trans ?_