awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))
have refine : 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) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
    (ENNReal.ofReal
      (rexp
        (-Real.log
              (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                    ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
          HPow.hPow (α := ℝ) 2 n)))
Tactic: refine (measure_gt_normThreshold_le_rpow h_rot ha_gt n).trans_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∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 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) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))
have e_a : 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 =
  ENNReal.ofReal
    (rexp
      (-Real.log
            (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                  ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
        HPow.hPow (α := ℝ) 2 n))
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 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 =
    ENNReal.ofReal
      (rexp
        (-Real.log
              (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                    ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
          HPow.hPow (α := ℝ) 2 n))
have e_a : 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 =
  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
Tactic: rw [← Real.log_inv, mul_comm (Real.log _), ← Real.log_rpow (by positivity),
    Real.exp_log (by positivity), ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity),
    ENNReal.toReal_div, inv_div, ← ENNReal.toReal_div, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
e_a :
  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 =
    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
⊢ 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 =
    ENNReal.ofReal
      (rexp
        (-Real.log
              (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                    ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
          HPow.hPow (α := ℝ) 2 n))
have e_a₁ : 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: rw [← Real.log_inv, mul_comm (Real.log _), ← Real.log_rpow (by positivity),
    Real.exp_log (by positivity), ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity),
    ENNReal.toReal_div, inv_div, ← ENNReal.toReal_div, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 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 =
    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 e_a : 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 =
  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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < logRatio c
have refine : 1 < c.toReal / (1 - c).toReal
Tactic: refine div_pos (Real.log_pos ?_) (by positivity)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < c.toReal / (1 - c).toReal
have rw : 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
Tactic: rw [one_lt_div_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
have refine_1 : 0 < (1 - c).toReal
Tactic: refine Or.inl ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_1 : 0 < (1 - c).toReal
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
have refine_2 : (1 - c).toReal < c.toReal
Tactic: refine Or.inl ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal
have refine_1 : 1 - c < ∞
Tactic: simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ (1 - c).toReal < c.toReal
have refine_2 : 1 - c < c
Tactic: refine (ENNReal.toReal_lt_toReal (by finiteness) (by finiteness)).mpr ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c < c
have refine_2 : 1 < c + c
Tactic: refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < c + c
have refine_2 : 1 < 2 * c
Tactic: rw [← two_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < 2 * c
have refine_2 : ∀ (hc_gt : 1 / 2 < c) (hc_lt : c < 1), 1 < 2 * c
Tactic: rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
Cleared hypotheses: hc_gt, hc_lt
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : ∀ (hc_gt : 1 / 2 < c) (hc_lt : c < 1), 1 < 2 * c
⊢ 1 < 2 * c
have refine_2₁ : ∀ (hc_gt : 1 < c * 2) (hc_lt : c < 1), 1 < 2 * c
Tactic: rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
Cleared hypotheses: hc_gt, hc_lt
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : ∀ (hc_gt : 1 / 2 < c) (hc_lt : c < 1), 1 < 2 * c
refine_2₁ : ∀ (hc_gt : 1 < c * 2) (hc_lt : c < 1), 1 < 2 * c
⊢ 1 < 2 * c
have refine_2₂ : ∀ (hc_gt : 1 < 2 * c) (hc_lt : c < 1), 1 < 2 * c
Tactic: rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
Cleared hypotheses: hc_gt, hc_lt
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
⊢ 0 ≤ logRatio c
have inl : c = 2⁻¹ → 0 ≤ logRatio c
Tactic: cases hc_ge.eq_or_lt'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
inl : c = 2⁻¹ → 0 ≤ logRatio c
⊢ 0 ≤ logRatio c
have inr : 2⁻¹ < c → 0 ≤ logRatio c
Tactic: cases hc_ge.eq_or_lt'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
⊢ 0 ≤ logRatio c
have inr : 1 = c → 0 ≤ logRatio c
Tactic: cases hc_le.eq_or_lt'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
inr : 1 = c → 0 ≤ logRatio c
⊢ 0 ≤ logRatio c
have inr₁ : c < 1 → 0 ≤ logRatio c
Tactic: cases hc_le.eq_or_lt'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) ≤
    Real.log (d.toReal / (1 - d).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2)
have hab : 0 < c.toReal / (1 - c).toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal / (1 - c).toReal
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) ≤
    Real.log (d.toReal / (1 - d).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2)
have hab₁ : 0 < (1 - d).toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal / (1 - c).toReal
hab₁ : 0 < (1 - d).toReal
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) ≤
    Real.log (d.toReal / (1 - d).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2)
have hab₂ : d ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal / (1 - c).toReal
hab₁ : 0 < (1 - d).toReal
hab₂ : d ≠ ∞
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) ≤
    Real.log (d.toReal / (1 - d).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2)
have hab₃ : 1 - c ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c.toReal / (1 - c).toReal
have hab : 0 < c.toReal
Tactic: refine div_pos ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal
⊢ 0 < c.toReal / (1 - c).toReal
have hab₁ : 0 < (1 - c).toReal
Tactic: refine div_pos ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c.toReal
have hab : 0 < c ∧ c < ∞
Tactic: rw [ENNReal.toReal_pos_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - c).toReal
have hab : c < 1 ∧ 1 - c < ∞
Tactic: simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < (1 - d).toReal
have hab : 1 - d < ∞
Tactic: simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hd, true_and]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
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
have 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
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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
⊢ 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
have 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
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
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
have pos : 0 ≤ Real.log (c.toReal / (1 - c).toReal)
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 0 ≤ Real.log (c.toReal / (1 - c).toReal)
have pos : 1 ≤ c.toReal / (1 - c).toReal
Tactic: refine Real.log_nonneg ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 ≤ c.toReal / (1 - c).toReal
have pos : (1 - c).toReal ≤ c.toReal
Tactic: rw [one_le_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
pos : (1 - c).toReal ≤ c.toReal
⊢ 1 ≤ c.toReal / (1 - c).toReal
have pos₁ : 0 < (1 - c).toReal
Tactic: rw [one_le_div]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ (1 - c).toReal ≤ c.toReal
have pos : 1 - c ≤ c
Tactic: refine (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 - c ≤ c
have pos : 1 ≤ c + c
Tactic: refine tsub_le_iff_left.mpr ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 ≤ c + c
have pos : 1 ≤ 2 * c
Tactic: rw [← two_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 1 ≤ 2 * c
have pos : ∀ (hc_gt : 1 < 2 * c) (hc_lt : c < 1) (n : ℕ) (ha : a = 0), 1 ≤ 2 * c
Tactic: rw [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
Cleared hypotheses: hc_gt, hc_lt, n, ha
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 0 < (1 - c).toReal
have pos : 1 - c < ∞
Tactic: simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ 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
have hbc : 0 ≤ logRatio c
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
hbc : 0 ≤ logRatio c
⊢ 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
have hbc₁ : HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
  HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
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
have 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
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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
⊢ 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
have 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
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