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

Tactic:
measure_gt_normThreshold_le_exp h_rot ha_gt ha_lt n

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

Tactic:
exact measure_gt_normThreshold_le_exp h_rot ha_gt ha_lt n

Premises used: ProbabilityTheory.Fernique.measure_gt_normThreshold_le_exp
-- 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 : C * HPow.hPow (β := ℕ) (t (n + 1)) 2 ≤ 2⁻¹ * Real.log (c.toReal / (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)) ≤
    ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
gcongr ENNReal.ofReal (rexp ?_) * _ * _

Premises used: ENNReal.ofReal, Real.exp
-- 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
⊢ logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 *
      HPow.hPow (β := ℕ) a⁻¹ 2 ≤
    2⁻¹ *
        Real.log
          (ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) /
            (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)).toReal) *
      HPow.hPow (α := ℝ) 2 n

Tactic:
logRatio_mul_normThreshold_add_one_le ha_gt ha_lt n (a := a)

Premises used: ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le
-- 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
h :
  C * HPow.hPow (β := ℕ) (t (n + 1)) 2 =
    logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 *
      HPow.hPow (β := ℕ) a⁻¹ 2
⊢ C * HPow.hPow (β := ℕ) (t (n + 1)) 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
convert! logRatio_mul_normThreshold_add_one_le ha_gt ha_lt n (a := a) using 1

Premises used: ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_le
-- 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
⊢ C * HPow.hPow (β := ℕ) (t (n + 1)) 2 =
    logRatio ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}) * HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 *
      HPow.hPow (β := ℕ) a⁻¹ 2

Tactic:
ring
-- 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
⊢ 0 ≤ rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)

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
rw :
  c *
      ENNReal.ofReal
        (rexp
          (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
            -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))
⊢ ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
rw [mul_comm _ c, mul_assoc, ← ENNReal.ofReal_mul (by positivity), ← Real.exp_add]

Premises used: ENNReal.ofReal_mul, mul_assoc, mul_comm, Real.exp_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
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
e_a :
  2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
      -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n
⊢ c *
      ENNReal.ofReal
        (rexp
          (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
            -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n))

Tactic:
congr
-- 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
e_a :
  2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) +
      -Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ)
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
      -Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * HPow.hPow (α := ℝ) 2 n

Tactic:
norm_cast
-- 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
e_a :
  2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
      -Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n =
    -2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) +
      -Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ) =
    -2⁻¹ * Real.log (c / (1 - c)).toReal * (↑(HPow.hPow (α := ℕ) 2 n) : ℝ)

Tactic:
simp only [Nat.cast_pow, Nat.cast_ofNat, ENNReal.toReal_div]

Premises used: Nat.cast_ofNat, Nat.cast_pow, ENNReal.toReal_div
-- 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
⊢ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n +
      -Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n =
    -2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * HPow.hPow (α := ℝ) 2 n

Tactic:
ring
-- 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_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
⊢ c' ≤ 1

Tactic:
have hc'_le : c' ≤ 1 := hc'.trans 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 μ
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
change :
  ∫⁻ (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)))
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * HPow.hPow (β := ℕ) a⁻¹ 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    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)))

Tactic:
change ∫⁻ x, .ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
      ≤ c * (.ofReal (rexp (logRatio c'))
            + ∑' n, .ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Premises used: HAdd.hAdd, tsum, SummationFilter.unconditional
-- 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_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
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 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_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
refine :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) (closedBall 0 a) x),
    ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))
⊢ ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 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_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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) x
h : 0 ≤ C
h₁ : ‖x‖ ≤ a
⊢ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) ≤ ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 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_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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) 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_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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) x
⊢ 0 ≤ C

Tactic:
exact mul_nonneg (logRatio_nonneg hc'_gt.le hc'_le) (by positivity)

Premises used: mul_nonneg, LT.lt.le, ProbabilityTheory.Fernique.logRatio_nonneg
-- 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_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
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 a) x
⊢ ‖x‖ ≤ a

Tactic:
simpa using hx
-- 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_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
simp :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)))
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
⊢ ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)) ∂μ =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))

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

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_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
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞)
      (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2)))
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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_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
simp :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞)
      (ENNReal.ofReal (rexp (logRatio c' * (HPow.hPow (β := ℕ) a 2)⁻¹ * HPow.hPow (β := ℕ) a 2))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 a) : ℝ≥0∞)
      (ENNReal.ofReal (rexp (C * HPow.hPow (β := ℕ) a 2))) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (ENNReal.ofReal (rexp (logRatio c')))

Tactic:
simp only [inv_pow, C]

Premises used: inv_pow