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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
L : StrongDual ℝ E
rw :
  HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ)
      (∫ (a : E),
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y ∂μ) =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
⊢ ∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)

Tactic:
rw [integral_add (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
L : StrongDual ℝ E
⊢ HAdd.hAdd (α := ℝ) (∫ (a : E), (L : (a : E) → ℝ) a ∂μ)
      (∫ (a : E),
        @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
          (L : (a : E) → ℝ) y ∂μ) =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)

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 : SecondCountableTopology E
L : StrongDual ℝ E
⊢ AEMeasurable (β := E) (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ

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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (α := E) (β := ℝ) (m₀ := inst_2) (⇑L : (a : E) → ℝ)
    (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
L : StrongDual ℝ E
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (∫ (x : E), (L : (a : E) → ℝ) ((ContinuousLinearEquiv.neg ℝ : (a : E) → E) x : E) ∂μ) =
    0
⊢ HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y) =
    0

Tactic:
rw [integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- 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 : SecondCountableTopology E
L : StrongDual ℝ E
⊢ HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (∫ (x : E), (L : (a : E) → ℝ) ((ContinuousLinearEquiv.neg ℝ : (a : E) → E) x : E) ∂μ) =
    0

Tactic:
simp [integral_neg]

Premises used: MeasureTheory.integral_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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : SecondCountableTopology E
L : StrongDual ℝ E
calc :
  Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    (∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ)
calc₁ :
  ∫ (x : E),
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ)
        (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
            (L : (a : E) → ℝ) y :
          ℝ) ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y)
calc₂ :
  HAdd.hAdd (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ)
      (@integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        (L : (a : E) → ℝ) y) =
    0
⊢ Eq (α := ℝ)
    (∫ (x : E),
      @integral _ _ _ _ inst_2 (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ) fun (y : E) ↦
        HAdd.hAdd (α := ℝ) (β := ℝ) ((L : (a : E) → ℝ) x : ℝ) ((L : (a : E) → ℝ) y : ℝ) ∂μ)
    0

Tactic:
calc ∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
  _ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ := by
    congr with x
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
  _ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) := by
    rw [integral_add (by fun_prop) (by fun_prop)]
    simp
  _ = 0 := by
    rw [integral_map (by fun_prop) (by fun_prop)]
    simp [integral_neg]

Premises used: Real, ContinuousLinearEquiv.neg, MeasureTheory.Measure.map, DFunLike.coe
-- 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
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
    (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

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
⊢ (∀ᵐ (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)‖)
      μ

Tactic:
rw [integrable_conv_iff (by fun_prop)] at hint

Premises used: MeasureTheory.integrable_conv_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 : 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
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)‖)
      μ
⊢ 0 < C'

Tactic:
rw [integrable_conv_iff (by fun_prop)] at hint

Premises used: MeasureTheory.integrable_conv_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 : 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
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'
⊢ C' < C

Tactic:
rw [integrable_conv_iff (by fun_prop)] at hint

Premises used: MeasureTheory.integrable_conv_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 : 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
⊢ ∀ᵐ (x : E) ∂μ,
    @Integrable ℝ _ _ _ inst_2 (fun (y : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x + y‖ 2))
      (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ) : (a : E) → E) μ)

Tactic:
replace hC := hint.1
-- 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 :
  (∀ᵐ (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) μ)
h :
  ∀ (y : E)
    (hy : @Integrable ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)),
    Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ
⊢ ∀ᵐ (y : E) ∂μ, Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ

Tactic:
filter_upwards [hC] with y hy
-- 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 :
  (∀ᵐ (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 ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_2) (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2))
    (Measure.map (-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 : 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 ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)
⊢ AEMeasurable (-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 : 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 ℝ _ _ _ inst_2 (fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) (Measure.map (-id) μ)
⊢ Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ

Tactic:
rw [integrable_map_measure (by fun_prop) (by fun_prop)] at hy

Premises used: MeasureTheory.integrable_map_measure
-- 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 :
  (∀ᵐ (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)) μ
⊢ Integrable (ε := ℝ) ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) μ

Tactic:
hy
-- 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 :
  (∀ᵐ (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)) μ
h :
  ∀ (x : E),
    rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2) = ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) x
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ

Tactic:
convert! hy 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 : 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
h : ‖x - y‖ = ‖y + -x‖ ∨ C = 0
⊢ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2) = ((fun (y_1 : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖y + y_1‖ 2)) ∘ (-id)) x

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₀]

Premises used: Real.exp_eq_exp, OfNat.ofNat_ne_zero, mul_eq_mul_left_iff, pow_left_inj₀, ne_eq, Function.comp_apply, not_false_eq_true, Pi.neg_apply, norm_nonneg, id_eq
-- 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 :
  (∀ᵐ (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
h : ‖x - y‖ = ‖y + -x‖
⊢ ‖x - y‖ = ‖y + -x‖ ∨ C = 0

Tactic:
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 : 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
h : ‖x - y‖ = ‖y - x‖
⊢ ‖x - y‖ = ‖y + -x‖

Tactic:
simp_rw [← sub_eq_add_neg, norm_sub_rev]

Premises used: sub_eq_add_neg, norm_sub_rev
-- 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
⊢ ∀ᵐ (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]
-- 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), Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x - y‖ 2)) μ

Tactic:
h_int.exists

Premises used: Filter.Eventually.exists
-- 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)) μ
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)) μ
⊢ 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

Premises used: Filter.Eventually.exists
-- 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'
rwa rwa₁ rwa₂ rwa₃ : C' < C
⊢ 0 < C - C'

Tactic:
rwa [sub_pos]

Premises used: sub_pos