awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
hε : 0 < ε
x : E
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
have h_le : 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
-- 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 : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2)
have ha : 0 ≤ C'
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
h_le : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ (1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖y‖ 2
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
have calc : C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C' * ((1 + ε) * HPow.hPow (β := ℕ) ‖x - y‖ 2 + (1 + 1 / ε) * HPow.hPow (β := ℕ) ‖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
-- 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 : 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)
⊢ C' * HPow.hPow (β := ℕ) ‖x‖ 2 ≤ C / ε * HPow.hPow (β := ℕ) ‖y‖ 2 + C * HPow.hPow (β := ℕ) ‖x - y‖ 2
have 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
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
-- 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
inst_5 : CompleteSpace E
μ : Measure E
inst_6 : IsGaussian μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have 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)) μ
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 (μ := μ)) _)
-- 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
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 : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have refine : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C / 2 * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: refine ⟨C / 2, 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 : 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 id p μ
have rw : MemLp (ε := ℝ) (fun (x : E) ↦ ‖id x‖ ^ ENNReal.toReal 2) (p / 2) μ
Tactic: rw [← memLp_norm_rpow_iff (q := 2) (by fun_prop) (by simp) (by simp)]
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p μ
have suffices : MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
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
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) (p / 2) μ
have lift : ∀ (p : ℝ≥0), MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ((↑p : ℝ≥0∞) / 2) μ
Tactic: lift p to ℝ≥0 using hp
Cleared hypotheses: p, hp
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ((↑p : ℝ≥0∞) / 2) μ
have h : (↑p : ℝ≥0∞) / 2 = (↑(p / 2) : ℝ≥0∞)
Tactic: convert! memLp_of_mem_interior_integrableExpSet ?_ (p / 2)
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
h : (↑p : ℝ≥0∞) / 2 = (↑(p / 2) : ℝ≥0∞)
⊢ MemLp (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) ((↑p : ℝ≥0∞) / 2) μ
have convert_5 : 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
Tactic: convert! memLp_of_mem_interior_integrableExpSet ?_ (p / 2)
-- 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 : CompleteSpace E
inst_5 : SecondCountableTopology E
μ : Measure E
inst_6 : IsGaussian μ
p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
have 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) μ)
Tactic: obtain ⟨C, hC_pos, hC⟩ := exists_integrable_exp_sq μ
-- 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 : 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)) μ
have refine : (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) 1
Tactic: refine integrable_of_le_of_le (g₁ := 0) (g₂ := 1) (by fun_prop)
      (ae_of_all _ fun _ ↦ by positivity) ?_ (integrable_const _) (integrable_const _)
-- 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 : 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)) μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : E) ↦ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2)) 1
have h : ∀ (x : E), rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 x
Tactic: filter_upwards with x
-- 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 : 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
⊢ rexp (-C * HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 x
have h : 0 ≤ C * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: simp only [neg_mul, Pi.one_apply, Real.exp_le_one_iff, Left.neg_nonpos_iff]
-- 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 : 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)) μ
⊢ 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
have hC_neg : 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
-- 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 : 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) μ)
have rw : Set.Ioo (-C) C ⊆ integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ
Tactic: rw [IsOpen.subset_interior_iff isOpen_Ioo]
-- 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 : 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)) μ
⊢ 0 ∈ interior (integrableExpSet (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ)
have h_subset : 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
-- 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
μ : 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 ∂μ)
have refine : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)))
Tactic: refine Measure.ext_of_charFunDual ?_
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
⊢ Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)))
have h₁ : ∀ (L : StrongDual ℝ E), charFunDual μ L = charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)) L
Tactic: ext L
-- 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
μ : 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
⊢ charFunDual μ L = charFunDual (mE := inst_2) (Measure.dirac (∫ (x : E), x ∂μ)) L
have h₁ : cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I - (↑0 : ℂ) / 2) =
  cexp ((↑((L : (a : E) → ℝ) (∫ (x : E), x ∂μ)) : ℂ) * I)
Tactic: rw [charFunDual_dirac, charFunDual_eq L, h L, integral_complex_ofReal, integral_dual L]
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ ∃ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
have contrapose! : ∀ (h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0), ∃ (x : E), μ = Measure.dirac x
Tactic: contrapose! h
Cleared hypotheses: h
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (L : StrongDual ℝ E) (hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨L, hL⟩ : ∃ L : StrongDual ℝ E, Var[L; μ] ≠ 0 := by
      contrapose! h
      exact ⟨_, eq_dirac_of_variance_eq_zero h⟩
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ NoAtoms (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
have rw : NoAtoms (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
Tactic: rw [map_eq_gaussianReal L]
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ NoAtoms (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
have refine : Var[(⇑L : (a : E) → ℝ); μ].toNNReal ≠ 0
Tactic: refine noAtoms_gaussianReal ?_
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ Var[(⇑L : (a : E) → ℝ); μ].toNNReal ≠ 0
have simp : 0 < Var[(⇑L : (a : E) → ℝ); μ]
Tactic: simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (⇑L : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have this : NoAtoms (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: have : NoAtoms (μ.map L) := by
        rw [map_eq_gaussianReal L]
        refine noAtoms_gaussianReal ?_
        simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
        exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
this : NoAtoms (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (⇑L : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [measure_singleton]
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have hL_zero : Eq (α := ℝ≥0∞)
  ((Measure.map (⇑L : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: have hL_zero : μ.map L {L x} = 0 := by
      have : NoAtoms (μ.map L) := by
        rw [map_eq_gaussianReal L]
        refine noAtoms_gaussianReal ?_
        simp only [ne_eq, Real.toNNReal_eq_zero, not_le]
        exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm
      rw [measure_singleton]
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
hL_zero :
  Eq (α := ℝ≥0∞)
    ((Measure.map (⇑L : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have hL_zero₁ : Eq (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply (by fun_prop) (measurableSet_singleton _)] at hL_zero
Cleared hypotheses: hL_zero
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
hL_zero :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : Subset (α := Set E) {x} (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)))
Tactic: refine measure_mono_null ?_ hL_zero
-- 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), id x ∂μ) 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (-(↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)
have refine : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
Tactic: refine charFunDual_eq_of_forall_strongDual_eq_zero (fun L ↦ ?_) L