awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : c < 1 ∧ 1 - c < ∞
⊢ 0 < (1 - c).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]

Premises used: ENNReal.toReal_pos_iff, tsub_pos_iff_lt
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c < ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ c < 1 ∧ 1 - c < ∞

Tactic:
exact ⟨h.trans_lt hd, by finiteness⟩
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 1 - d < ∞
⊢ 0 < (1 - d).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hd, true_and]

Premises used: ENNReal.toReal_pos_iff, tsub_pos_iff_lt, true_and
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - d < ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 1 - c ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
pos :
  ∀ (ha : a = 0),
    logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
      2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
neg :
  ∀ (ha : ¬a = 0),
    logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
      2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
⊢ logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 0 ≤ Real.log (c.toReal / (1 - c).toReal)
⊢ logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      Nat.ofNat_pos, pow_pos, mul_nonneg_iff_of_pos_right, inv_pos, mul_nonneg_iff_of_pos_left]

Premises used: mul_nonneg_iff_of_pos_right, pow_pos, OfNat.ofNat_ne_zero, inv_zero, inv_pos, Nat.ofNat_pos, ne_eq, MulZeroClass.mul_zero, mul_nonneg_iff_of_pos_left, not_false_eq_true, zero_pow
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 0 ≤ Real.log (c.toReal / (1 - c).toReal)

Tactic:
Real.log_nonneg ?_

Premises used: Real.log_nonneg
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 1 ≤ c.toReal / (1 - c).toReal
⊢ 0 ≤ Real.log (c.toReal / (1 - c).toReal)

Tactic:
refine Real.log_nonneg ?_

Premises used: Real.log_nonneg
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : (1 - c).toReal ≤ c.toReal
pos₁ : 0 < (1 - c).toReal
⊢ 1 ≤ c.toReal / (1 - c).toReal

Tactic:
rw [one_le_div]

Premises used: one_le_div
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ c ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 1 - c ≤ c
⊢ (1 - c).toReal ≤ c.toReal

Tactic:
refine (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr ?_

Premises used: Iff.mpr, ENNReal.toReal_le_toReal
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c ≤ c

Tactic:
tsub_le_iff_left.mpr ?_

Premises used: Iff.mpr, tsub_le_iff_left
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 1 ≤ c + c
⊢ 1 - c ≤ c

Tactic:
refine tsub_le_iff_left.mpr ?_

Premises used: Iff.mpr, tsub_le_iff_left
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 1 ≤ 2 * c
⊢ 1 ≤ c + c

Tactic:
rw [← two_mul]

Premises used: two_mul
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 1 / 2 < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ Ne (α := ℝ≥0∞) 2 0 ∨ Ne (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 1 / 2 < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ Ne (α := ℝ≥0∞) 2 ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : ∀ (hc_gt : 1 < 2 * c) (hc_lt : c < 1) (n : ℕ) (ha : a = 0), 1 ≤ 2 * c
⊢ 1 ≤ 2 * c

Tactic:
rw [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt

Premises used: inv_eq_one_div, mul_comm, ENNReal.div_lt_iff
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 1 < 2 * c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 ≤ 2 * c

Tactic:
hc_gt.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 1 < 2 * c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 ≤ 2 * c

Tactic:
exact hc_gt.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : 1 - c < ∞
⊢ 0 < (1 - c).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]

Premises used: ENNReal.toReal_pos_iff, tsub_pos_iff_lt, true_and
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c < ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
hbc : 0 ≤ logRatio c
hbc₁ :
  HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
    HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)
⊢ logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    logRatio c * (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)) *
      HPow.hPow (β := ℕ) a⁻¹ 2

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ 0 ≤ logRatio c

Tactic:
(logRatio_pos hc_gt hc_lt).le

Premises used: LT.lt.le, ProbabilityTheory.Fernique.logRatio_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ 0 ≤ logRatio c

Tactic:
exact (logRatio_pos hc_gt hc_lt).le

Premises used: LT.lt.le, ProbabilityTheory.Fernique.logRatio_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
    HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
sq_normThreshold_add_one_le n

Premises used: ProbabilityTheory.Fernique.sq_normThreshold_add_one_le
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
    HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
exact sq_normThreshold_add_one_le n

Premises used: ProbabilityTheory.Fernique.sq_normThreshold_add_one_le
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) *
        (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)) *
      HPow.hPow (β := ℕ) a⁻¹ 2 =
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
calc :
  logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    logRatio c * (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)) *
      HPow.hPow (β := ℕ) a⁻¹ 2
calc₁ :
  logRatio c * (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)) *
      HPow.hPow (β := ℕ) a⁻¹ 2 =
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
⊢ logRatio c * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 * HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
calc logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2
  _ ≤ logRatio c * (a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)) * a⁻¹ ^ 2 := by
    gcongr
    · exact (logRatio_pos hc_gt hc_lt).le
    · exact sq_normThreshold_add_one_le n
  _ = 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n := by
    unfold logRatio
    field

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.log, ProbabilityTheory.Fernique.normThreshold, ENNReal.toReal, HPow.hPow, HAdd.hAdd, Real.sqrt, ProbabilityTheory.Fernique.logRatio, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Fernique
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
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))
⊢ ∫⁻ (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)) ∂μ

Tactic:
refine setLIntegral_mono (by fun_prop) fun x hx ↦ ?_

Premises used: MeasureTheory.setLIntegral_mono
-- Module: Mathlib.Probability.Distributions.Fernique
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
h₁ : ‖x‖ ≤ t (n + 1)
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) (t (n + 1)) 2))

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ 0 ≤ HPow.hPow (β := ℕ) a⁻¹ 2

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ 0 ≤ C

Tactic:
exact mul_nonneg (logRatio_pos ha_gt ha_lt).le (by positivity)

Premises used: mul_nonneg, LT.lt.le, ProbabilityTheory.Fernique.logRatio_pos
-- Module: Mathlib.Probability.Distributions.Fernique
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) ∧ t n < ‖x‖

Tactic:
simp only [Set.mem_diff, mem_closedBall, dist_zero_right, not_le] at hx

Premises used: not_le, Set.mem_diff, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Probability.Distributions.Fernique
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 : ‖x‖ ≤ t (n + 1) ∧ t n < ‖x‖
⊢ ‖x‖ ≤ t (n + 1)

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Probability.Distributions.Fernique
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 : ‖x‖ ≤ t (n + 1) ∧ t n < ‖x‖
⊢ ‖x‖ ≤ t (n + 1)

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Probability.Distributions.Fernique
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 (β := ℕ) (t (n + 1)) 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∞)

Tactic:
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, C, t]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.Probability.Distributions.Fernique
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
bc : Subset.{u_1} (α := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) {x : E | t n < ‖x‖}
⊢ 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∞)

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ Membership.mem (γ := Set E) (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) x →
    Membership.mem (γ := Set E) {x : E | t n < ‖x‖} x

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
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
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)))
| 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]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Distributions.Fernique
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
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)))
⊢ 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]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Distributions.Fernique
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
bc :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | t n < ‖x‖} ≤
    c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ 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:
gcongr