awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
⊢ 0 < C'

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
⊢ 0 < ε

Tactic:
have hε : 0 < ε := div_pos (by rwa [sub_pos]) (by positivity)
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
refine_1 : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)
refine_2 :
  (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) fun (x : E) ↦
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
refine integrable_of_le_of_le (g₁ := 0)
      (g₂ := fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)) (by fun_prop) ?_ ?_
      (integrable_const _) (hy.const_mul _)

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.integrable_of_le_of_le, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
x : E
⊢ LE.le (α := ℝ) (0 x) ((fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) x)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)

Tactic:
exact ae_of_all _ fun _ ↦ by positivity

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) fun (x : E) ↦
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)

Tactic:
ae_of_all _ this

Premises used: MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) fun (x : E) ↦
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)

Tactic:
exact ae_of_all _ this

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
suffices :
  ∀ (x : E),
    rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
      rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
suffices ∀ x, rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2) by
    refine integrable_of_le_of_le (g₁ := 0)
      (g₂ := fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)) (by fun_prop) ?_ ?_
      (integrable_const _) (hy.const_mul _)
    · exact ae_of_all _ fun _ ↦ by positivity
    · exact ae_of_all _ this
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
rw : rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
⊢ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)

Tactic:
rw [← Real.exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
a : C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
⊢ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2)

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x - y + y‖ 2

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
h₁ : LE.le (α := ℝ) 0 ‖x - y + y‖
grw grw₁ : HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2
⊢ HPow.hPow (β := ℕ) ‖x - y + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2

Tactic:
grw [norm_add_le (x - y) y]

Premises used: HSub.hSub, norm_add_le
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2 = HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
simp_rw :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 + (HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖) ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      (HPow.hPow (β := ℕ) ‖y‖ 2 + (ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2))
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖ ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simp_rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
bc : 2 * ‖x - y‖ * ‖y‖ ≤ ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 + (HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖) ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      (HPow.hPow (β := ℕ) ‖y‖ 2 + (ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2))

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ 0 < ε

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ 2 * ‖x - y‖ * ‖y‖ ≤ ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
exact two_mul_le_add_mul_sq (by positivity)

Premises used: two_mul_le_add_mul_sq
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2 =
    (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
calc : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x - y + y‖ 2
calc₁ : HPow.hPow (β := ℕ) ‖x - y + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2
calc₂ :
  HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2 = HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖
calc₃ :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖ ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2
calc₄ :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2 =
    (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
calc ‖x‖ ^ 2
    _ = ‖x - y + y‖ ^ 2 := by simp
    _ ≤ (‖x - y‖ + ‖y‖) ^ 2 := by grw [norm_add_le (x - y) y]
    _ = ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + 2 * ‖x - y‖ * ‖y‖ := by ring
    _ ≤ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + ε * ‖x - y‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2 := by
      simp_rw [add_assoc]
      gcongr
      exact two_mul_le_add_mul_sq (by positivity)
    _ = (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2 := by ring

Premises used: Norm.norm, HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have h_le : ‖x‖ ^ 2 ≤ (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2 := by
    calc ‖x‖ ^ 2
    _ = ‖x - y + y‖ ^ 2 := by simp
    _ ≤ (‖x - y‖ + ‖y‖) ^ 2 := by grw [norm_add_le (x - y) y]
    _ = ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + 2 * ‖x - y‖ * ‖y‖ := by ring
    _ ≤ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + ε * ‖x - y‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2 := by
      simp_rw [add_assoc]
      gcongr
      exact two_mul_le_add_mul_sq (by positivity)
    _ = (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2 := by ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
h_le : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 ≤ C'
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Gaussian.Fernique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsGaussian μ
C C' : ℝ
hint :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
y : E
hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
h_le : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2) =
    C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2

Tactic:
grind