awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ
x : E
⊢ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2) = ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) x
have h : ‖x - y‖ = ‖y + -x‖ ∨ C = 0
Tactic: simp only [Function.comp_apply, Pi.neg_apply, id_eq, Real.exp_eq_exp, mul_eq_mul_left_iff,
      norm_nonneg, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_left_inj₀]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y + -x‖ ∨ C = 0
have h : ‖x - y‖ = ‖y + -x‖
Tactic: left
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 :
  (∀ᵐ (x : E) ∂μ,
      @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
        (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)) ∧
    Integrable (ε := ℝ)
      (fun (x : E) ↦
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          ‖rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)‖)
      μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC :
  ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y + -x‖
have h : ‖x - y‖ = ‖y - x‖
Tactic: simp_rw [← sub_eq_add_neg, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (hypothesis)
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
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have h_int : ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
Tactic: have h_int : ∀ᵐ y ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ := by
    rw [integrable_conv_iff (by fun_prop)] at hint
    replace hC := hint.1
    simp only [ContinuousLinearEquiv.coe_neg] at hC
    filter_upwards [hC] with y hy
    rw [integrable_map_measure (by fun_prop) (by fun_prop)] at hy
    convert! hy with x
    simp only [Function.comp_apply, Pi.neg_apply, id_eq, Real.exp_eq_exp, mul_eq_mul_left_iff,
      norm_nonneg, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_left_inj₀]
    left
    simp_rw [← sub_eq_add_neg, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have obtain : ∀ (y : E) (hy : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ),
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: obtain ⟨y, hy⟩ : ∃ y, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ := h_int.exists
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (hypothesis)
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'
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have hε : 0 < ε
Tactic: have hε : 0 < ε := div_pos (by rwa [sub_pos]) (by positivity)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have refine_1 : (ae μ).EventuallyLE (β := ℝ) 0 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 _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have 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)
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 _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 < ε
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have suffices : ∀ (x : E),
  rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
⊢ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤
    rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2) * rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
have rw : rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
Tactic: rw [← Real.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
⊢ rexp (C' * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ rexp (C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2)
have a : C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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‖ + ‖y‖) 2
have h₁ : LE.le (α := ℝ) 0 ‖x - y + y‖
Tactic: grw [norm_add_le (x - y) y]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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‖
⊢ HPow.hPow (β := ℕ) ‖x - y + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2
have grw : HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2
Tactic: grw [norm_add_le (x - y) y]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 + 2 * ‖x - y‖ * ‖y‖ ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2
have 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))
Tactic: simp_rw [add_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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 + 2 * ‖x - y‖ * ‖y‖) ≤
    HPow.hPow (β := ℕ) ‖x - y‖ 2 +
      (HPow.hPow (β := ℕ) ‖y‖ 2 + (ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2))
have bc : 2 * ‖x - y‖ * ‖y‖ ≤ ε * HPow.hPow (β := ℕ) ‖x - y‖ 2 + ε⁻¹ * HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
have calc : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x - y + 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
have calc₁ : HPow.hPow (β := ℕ) ‖x - y + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x - y‖ + ‖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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
have calc₂ : HPow.hPow (β := ℕ) (‖x - y‖ + ‖y‖) 2 = HPow.hPow (β := ℕ) ‖x - y‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2 + 2 * ‖x - y‖ * ‖y‖
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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‖
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
have 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
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Fernique (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
have 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
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