awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
⊢ 1 ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)))

Tactic:
le_add_right ?_

Premises used: le_add_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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
inl : 1 ≤ ENNReal.ofReal (rexp (logRatio c))
⊢ 1 ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-(2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)))

Tactic:
refine le_add_right ?_

Premises used: le_add_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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
inl : ENNReal.ofReal 1 ≤ ENNReal.ofReal (rexp (logRatio c))
⊢ 1 ≤ ENNReal.ofReal (rexp (logRatio c))

Tactic:
rw [← ENNReal.ofReal_one]

Premises used: ENNReal.ofReal_one
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
inl : 1 ≤ rexp (logRatio c)
⊢ ENNReal.ofReal 1 ≤ ENNReal.ofReal (rexp (logRatio c))

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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
inl : 0 ≤ logRatio c
⊢ 1 ≤ rexp (logRatio c)

Tactic:
simp only [Real.one_le_exp_iff]

Premises used: Real.one_le_exp_iff
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
⊢ 0 ≤ logRatio c

Tactic:
logRatio_nonneg hc_gt.le (hc.trans prob_le_one)

Premises used: MeasureTheory.prob_le_one, LT.lt.le, ProbabilityTheory.Fernique.logRatio_nonneg, LE.le.trans
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha_1 : 0 ≤ a
ha : a = 0
⊢ 0 ≤ logRatio c

Tactic:
exact logRatio_nonneg hc_gt.le (hc.trans prob_le_one)

Premises used: MeasureTheory.prob_le_one, LT.lt.le, ProbabilityTheory.Fernique.logRatio_nonneg, LE.le.trans
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
(lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_

Premises used: ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul, LE.le.trans
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
inr :
  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))) ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
refine (lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_

Premises used: ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul, LE.le.trans
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
rw :
  1 *
    (ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))
| ENNReal.ofReal (rexp (logRatio c)) +
    ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
rw [← one_mul (ENNReal.ofReal _ + _)]

Premises used: ENNReal.ofReal, HAdd.hAdd, one_mul
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
inr :
  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))) ≤
    1 *
      (ENNReal.ofReal (rexp (logRatio c)) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))
⊢ 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))) ≤
    ENNReal.ofReal (rexp (logRatio c)) +
      ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
conv_rhs => rw [← one_mul (ENNReal.ofReal _ + _)]

Premises used: ENNReal.ofReal, HAdd.hAdd, one_mul
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
inr : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ 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))) ≤
    1 *
      (ENNReal.ofReal (rexp (logRatio c)) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)))

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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
prob_le_one

Premises used: MeasureTheory.prob_le_one
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
ha_pos : 0 < a
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact prob_le_one

Premises used: MeasureTheory.prob_le_one
-- 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 μ
c : ℝ≥0∞
hc : c ≤ (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
ha : 0 ≤ a
⊢ a = 0 ∨ 0 < a

Tactic:
cases ha.eq_or_lt' with
  | inl ha =>
    simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      zero_mul, Real.exp_zero, ENNReal.ofReal_one, lintegral_const, measure_univ, mul_one,
      ENNReal.toReal_div, neg_mul]
    refine le_add_right ?_
    rw [← ENNReal.ofReal_one]
    gcongr
    simp only [Real.one_le_exp_iff]
    exact logRatio_nonneg hc_gt.le (hc.trans prob_le_one)
  | inr ha_pos =>
  refine (lintegral_exp_mul_sq_norm_le_mul h_rot ha_pos hc hc_gt).trans ?_
  conv_rhs => rw [← one_mul (ENNReal.ofReal _ + _)]
  gcongr
  exact prob_le_one

Premises used: MeasureTheory.lintegral_const, Real.one_le_exp_iff, OfNat.ofNat_ne_zero, ENNReal.ofReal, inv_zero, MulZeroClass.zero_mul, MeasureTheory.prob_le_one, MeasureTheory.IsProbabilityMeasure.measure_univ, LT.lt.le, ne_eq, ENNReal.ofReal_one, MulZeroClass.mul_zero, HAdd.hAdd, ProbabilityTheory.Fernique.logRatio_nonneg, neg_mul, Real.exp_zero, LE.le.trans, mul_one, LE.le.eq_or_lt', not_false_eq_true, ENNReal.toReal_div, zero_pow, one_mul, le_add_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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
⊢ c < 1

Tactic:
replace hc_lt : c < 1 := ha_lt
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
⊢ c < ∞

Tactic:
have hc_lt_top : c < ∞ := measure_lt_top _ _
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
⊢ LT.lt (α := ℝ≥0∞) 1 2

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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
⊢ 1 - c < ∞

Tactic:
have hc_one_sub_lt_top : 1 - c < ∞ := lt_top_of_lt (b := 2) (tsub_le_self.trans_lt (by 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 1 - c < c

Tactic:
ENNReal.sub_lt_of_lt_add hc_lt.le ?_

Premises used: LT.lt.le, ENNReal.sub_lt_of_lt_add
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
refine : 1 < c + c
⊢ 1 - c < c

Tactic:
refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_

Premises used: LT.lt.le, ENNReal.sub_lt_of_lt_add
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
rw : 1 < 2 * c
⊢ 1 < c + c

Tactic:
rw [← two_mul]

Premises used: two_mul
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 1 / 2 < (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ Ne (α := ℝ≥0∞) 2 0 ∨ Ne (α := ℝ≥0∞) 1 0

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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
ha_gt : 1 / 2 < (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ Ne (α := ℝ≥0∞) 2 ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞

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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
rwa :
  ∀ (ha_gt : 1 / 2 < (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a})
    (ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)),
    let c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a};
    ∀ (hc_lt : c < 1) (hc_lt_top : c < ∞) (hc_one_sub_lt_top : 1 - c < ∞), 1 < 2 * c
rwa₁ :
  ∀ (ha_gt : 1 < HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2 : ℝ≥0∞))
    (ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)),
    let c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a};
    ∀ (hc_lt : c < 1) (hc_lt_top : c < ∞) (hc_one_sub_lt_top : 1 - c < ∞), 1 < 2 * c
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (ha_gt : 1 < HMul.hMul (α := ℝ≥0∞) (β := ℝ≥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∞)),
    let c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a};
    ∀ (hc_lt : c < 1) (hc_lt_top : c < ∞) (hc_one_sub_lt_top : 1 - c < ∞), 1 < 2 * c
⊢ 1 < 2 * c

Tactic:
rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at ha_gt

Premises used: inv_eq_one_div, mul_comm, ENNReal.div_lt_iff
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 1 - c < c

Tactic:
have h_one_sub_lt_self : 1 - c < c := by
    refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_
    rw [← two_mul]
    rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at ha_gt
-- 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
⊢ 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
ha_pos : 0 < a
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∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
h_one_sub_lt_self : 1 - c < c
⊢ 0 < logRatio c * HPow.hPow (β := ℕ) a⁻¹ 2

Tactic:
have h_pos : 0 < logRatio c * a⁻¹ ^ 2 := mul_pos (logRatio_pos ha_gt hc_lt) (by positivity)