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'
hε : 0 < ε
x : E
h_le : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
calc :
  C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2)
calc₁ :
  C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2) =
    C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2

Tactic:
calc C' * ‖x‖ ^ 2
  _ ≤ C' * ((1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2) := by gcongr
  _ = C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2 := by grind

Premises used: Norm.norm, HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
⊢ ∃ (C : ℝ),
    0 < C ∧
      Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
        (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
exists_integrable_exp_sq_of_map_rotation_eq_self
      (map_rotation_eq_self_of_forall_strongDual_eq_zero
        (integral_dual_conv_map_neg_eq_zero (μ := μ)) _)

Premises used: ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero
-- 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
obtain :
  ∀ (C : ℝ) (hC_pos : 0 < C)
    (hC :
      Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
        (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)),
    ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
obtain ⟨C, hC_pos, hC⟩ : ∃ C, 0 < C
      ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ μ.map (ContinuousLinearEquiv.neg ℝ)) :=
    exists_integrable_exp_sq_of_map_rotation_eq_self
      (map_rotation_eq_self_of_forall_strongDual_eq_zero
        (integral_dual_conv_map_neg_eq_zero (μ := μ)) _)

Premises used: ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero
-- 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
⊢ 0 < C / 2

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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
refine : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C / 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
refine ⟨C / 2, 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
⊢ C / 2 < C

Tactic:
simp [hC_pos]
-- 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC :
  Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C / 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
exact integrable_exp_sq_of_conv_neg μ hC (by positivity) (by simp [hC_pos])

Premises used: ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
⊢ AEStronglyMeasurable id μ

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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
⊢ Ne (α := ℝ≥0∞) 2 0

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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
⊢ Ne (α := ℝ≥0∞) 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
rw : MemLp (ε := ℝ) (fun (x : E) ↦ ‖id x‖ ^ ENNReal.toReal 2) (p / 2) μ
⊢ MemLp id p μ

Tactic:
rw [← memLp_norm_rpow_iff (q := 2) (by fun_prop) (by simp) (by simp)]

Premises used: MeasureTheory.memLp_norm_rpow_iff
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ ‖id x‖ ^ ENNReal.toReal 2) (p / 2) μ

Tactic:
simpa using 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
suffices : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
⊢ MemLp id p μ

Tactic:
suffices MemLp (fun x ↦ ‖x‖ ^ 2) (p / 2) μ by
    rw [← memLp_norm_rpow_iff (q := 2) (by fun_prop) (by simp) (by simp)]
    simpa using 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
⊢ p ≠ ∞

Tactic:
hp
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
lift : ∀ (p : ℝ≥0), MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ((↑p : ℝ≥0∞) / 2) μ
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ

Tactic:
lift p to ℝ≥0 using hp
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (↑(p / 2) : ℝ≥0∞) μ

Tactic:
memLp_of_mem_interior_integrableExpSet ?_ (p / 2)

Premises used: ProbabilityTheory.memLp_of_mem_interior_integrableExpSet, HDiv.hDiv, 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
h : (↑p : ℝ≥0∞) / 2 = (↑(p / 2) : ℝ≥0∞)
convert_5 : 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ((↑p : ℝ≥0∞) / 2) μ

Tactic:
convert! memLp_of_mem_interior_integrableExpSet ?_ (p / 2)

Premises used: ProbabilityTheory.memLp_of_mem_interior_integrableExpSet, HDiv.hDiv, 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
⊢ (↑p : ℝ≥0∞) / 2 = (↑(p / 2) : ℝ≥0∞)

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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
convert_5 :
  ∀ (C : ℝ) (hC_pos : 0 < C) (hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ),
    0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
⊢ 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)

Tactic:
obtain ⟨C, hC_pos, hC⟩ := exists_integrable_exp_sq μ

Premises used: ProbabilityTheory.IsGaussian.exists_integrable_exp_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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
refine : (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) 1
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
refine integrable_of_le_of_le (g₁ := 0) (g₂ := 1) (by fun_prop)
      (ae_of_all _ fun _ ↦ by positivity) ?_ (integrable_const _) (integrable_const _)

Premises used: MeasureTheory.integrable_of_le_of_le, MeasureTheory.ae_of_all, 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
h : ∀ (x : E), rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 x
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) 1

Tactic:
filter_upwards with x
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
x : E
h : 0 ≤ C * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 x

Tactic:
simp only [neg_mul, Pi.one_apply, Real.exp_le_one_iff, Left.neg_nonpos_iff]

Premises used: Pi.one_apply, Left.neg_nonpos_iff, neg_mul, Real.exp_le_one_iff
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
x : E
⊢ 0 ≤ C * HPow.hPow (β := ℕ) ‖x‖ 2

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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
have hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ := by -- `-C` could be any negative
    refine integrable_of_le_of_le (g₁ := 0) (g₂ := 1) (by fun_prop)
      (ae_of_all _ fun _ ↦ by positivity) ?_ (integrable_const _) (integrable_const _)
    filter_upwards with x
    simp only [neg_mul, Pi.one_apply, Real.exp_le_one_iff, Left.neg_nonpos_iff]
    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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
rw : Set.Ioo (-C) C ⊆ integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ
⊢ Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)

Tactic:
rw [IsOpen.subset_interior_iff isOpen_Ioo]

Premises used: isOpen_Ioo, IsOpen.subset_interior_iff
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ Set.Ioo (-C) C ⊆ integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ

Tactic:
fun x hx ↦ integrable_exp_mul_of_le_of_le hC_neg hC hx.1.le hx.2.le

Premises used: Set.Mem, setOf, MeasureTheory.Integrable, LT.lt.le, ProbabilityTheory.integrableExpSet, Set.Subset, ProbabilityTheory.integrable_exp_mul_of_le_of_le, And.right, And.left
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ Set.Ioo (-C) C ⊆ integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ

Tactic:
exact fun x hx ↦ integrable_exp_mul_of_le_of_le hC_neg hC hx.1.le hx.2.le

Premises used: ProbabilityTheory.integrable_exp_mul_of_le_of_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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)

Tactic:
have h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ) := by
    rw [IsOpen.subset_interior_iff isOpen_Ioo]
    exact fun x hx ↦ integrable_exp_mul_of_le_of_le hC_neg hC hx.1.le hx.2.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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
⊢ -C < 0

Tactic:
simp [hC_pos]
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
hC_neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
⊢ 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)

Tactic:
exact h_subset ⟨by simp [hC_pos], hC_pos⟩

Premises used: And.intro
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
norm_num
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
norm_num
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
L : StrongDual ℝ E
⊢ Ne (α := ℝ≥0∞) 1 ∞

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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
⊢ μ = Measure.dirac (∫ (x : E), x ∂μ)

Tactic:
Measure.ext_of_charFunDual ?_

Premises used: MeasureTheory.Measure.ext_of_charFunDual
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
refine :
  Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)))
⊢ μ = Measure.dirac (∫ (x : E), x ∂μ)

Tactic:
refine Measure.ext_of_charFunDual ?_

Premises used: MeasureTheory.Measure.ext_of_charFunDual
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
h₁ : ∀ (L : StrongDual ℝ E), charFunDual μ L = charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)) L
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)))

Tactic:
ext L
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
L : StrongDual ℝ E
h₁ :
  cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I - (↑0 : ℂ) / 2) =
    cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I)
⊢ charFunDual μ L = charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)) L

Tactic:
rw [charFunDual_dirac, charFunDual_eq L, h L, integral_complex_ofReal, integral_dual L]

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.IsGaussian.integral_dual, MeasureTheory.charFunDual_dirac, integral_complex_ofReal
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
L : StrongDual ℝ E
⊢ cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I - (↑0 : ℂ) / 2) =
    cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I)

Tactic:
simp