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

Tactic:
contrapose! h
-- 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
x : E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
⊢ ∃ (x : E), μ = Measure.dirac x

Tactic:
⟨_, eq_dirac_of_variance_eq_zero h⟩

Premises used: ProbabilityTheory.IsGaussian.eq_dirac_of_variance_eq_zero, Exists.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
x : E
h : ∀ (L : StrongDual ℝ E), Var[(⇑L : (a : E) → ℝ); μ] = 0
⊢ ∃ (x : E), μ = Measure.dirac x

Tactic:
exact ⟨_, eq_dirac_of_variance_eq_zero h⟩
-- 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 : ∀ (x : E), μ ≠ Measure.dirac x
x : E
obtain :
  ∀ (L : StrongDual ℝ E) (hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥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⟩

Premises used: Real, StrongDual
-- 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 : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
rw : NoAtoms (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)
⊢ NoAtoms (α := ℝ) (m0 := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
rw [map_eq_gaussianReal L]

Premises used: ProbabilityTheory.IsGaussian.map_eq_gaussianReal
-- 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 : ∀ (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)

Tactic:
noAtoms_gaussianReal ?_

Premises used: ProbabilityTheory.noAtoms_gaussianReal
-- 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 : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
refine : Var[(⇑L : (a : E) → ℝ); μ].toNNReal ≠ 0
⊢ NoAtoms (gaussianReal (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) Var[(⇑L : (a : E) → ℝ); μ].toNNReal)

Tactic:
refine noAtoms_gaussianReal ?_

Premises used: ProbabilityTheory.noAtoms_gaussianReal
-- 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 : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
simp : 0 < Var[(⇑L : (a : E) → ℝ); μ]
⊢ Var[(⇑L : (a : E) → ℝ); μ].toNNReal ≠ 0

Tactic:
simp only [ne_eq, Real.toNNReal_eq_zero, not_le]

Premises used: not_le, ne_eq, Real.toNNReal_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
μ : 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
⊢ 0 < Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
lt_of_le_of_ne (variance_nonneg _ _) hL.symm

Premises used: Ne.symm, ProbabilityTheory.variance_nonneg, lt_of_le_of_ne
-- 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 : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[(⇑L : (a : E) → ℝ); μ] ≠ 0
⊢ 0 < Var[(⇑L : (a : E) → ℝ); μ]

Tactic:
exact lt_of_le_of_ne (variance_nonneg _ _) hL.symm

Premises used: Ne.symm, ProbabilityTheory.variance_nonneg, lt_of_le_of_ne
-- 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 : ∀ (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) → ℝ) μ)

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
-- 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 : ∀ (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) → ℝ) μ)
rw rw₁ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (⇑L : (a : E) → ℝ) μ : (a : Set ℝ) → ℝ≥0∞) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton
-- 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 : ∀ (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∞)

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]
-- 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 : ∀ (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∞)
⊢ Measurable (α := E) (β := ℝ) (⇑L : (a : 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 : 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∞)
        (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

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.map_apply
-- 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 : ∀ (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∞)

Tactic:
measure_mono_null ?_ hL_zero

Premises used: MeasureTheory.measure_mono_null
-- 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 : ∀ (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∞)
refine :
  Subset (α := Set E) {x} (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null ?_ hL_zero

Premises used: MeasureTheory.measure_mono_null
-- 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 : ∀ (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∞)
⊢ Subset (α := Set E) {x} (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)))

Tactic:
fun ⦃a⦄ ↦ congrArg ⇑L

Premises used: congrArg, Set.Mem, setOf, Set.Subset, Set.preimage, Set.singleton, 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
μ : 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∞)
⊢ Subset (α := Set E) {x} (Set.preimage (β := ℝ) (⇑L : (a : E) → ℝ) (singleton (α := ℝ) ((L : (a : E) → ℝ) x : ℝ)))

Tactic:
exact fun ⦃a⦄ ↦ congrArg ⇑L

Premises used: congrArg, 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
μ : 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)

Tactic:
charFunDual_eq_of_forall_strongDual_eq_zero (fun L ↦ ?_) L

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq_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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), id x ∂μ) 0
L : StrongDual ℝ E
refine : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
⊢ charFunDual μ L = cexp (-(↑Var[(⇑L : (a : E) → ℝ); μ] : ℂ) / 2)

Tactic:
refine charFunDual_eq_of_forall_strongDual_eq_zero (fun L ↦ ?_) L

Premises used: ProbabilityTheory.IsGaussian.charFunDual_eq_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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), x ∂μ) 0
L_1 L : StrongDual ℝ E
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0

Tactic:
simp [integral_dual, hμ]

Premises used: ProbabilityTheory.IsGaussian.integral_dual
-- 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μ : Eq (α := E) (∫ (x : E), id x ∂μ) 0
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ

Tactic:
map_rotation_eq_self_of_forall_strongDual_eq_zero (fun L ↦ ?_) θ

Premises used: 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), id x ∂μ) 0
θ : ℝ
refine : ∀ (L : StrongDual ℝ E), Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ

Tactic:
refine map_rotation_eq_self_of_forall_strongDual_eq_zero (fun L ↦ ?_) θ

Premises used: 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
μ : Measure E
inst_4 : IsGaussian μ
inst_5 : CompleteSpace E
inst_6 : SecondCountableTopology E
hμ : Eq (α := E) (∫ (x : E), x ∂μ) 0
θ : ℝ
L : StrongDual ℝ E
⊢ Eq (α := ℝ) (∫ (x : E), (L : (a : E) → ℝ) x ∂μ) 0

Tactic:
simp [integral_dual, hμ]

Premises used: ProbabilityTheory.IsGaussian.integral_dual
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᶠ[ae P] Y
rw : IsGaussian (mE := mE) (Measure.map X P)
⊢ IsGaussian (mE := mE) (Measure.map Y P)

Tactic:
rw [← Measure.map_congr h]

Premises used: MeasureTheory.Measure.map_congr
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᶠ[ae P] Y
⊢ IsGaussian (mE := mE) (Measure.map X P)

Tactic:
hX.isGaussian_map

Premises used: ProbabilityTheory.HasGaussianLaw.isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᶠ[ae P] Y
⊢ IsGaussian (mE := mE) (Measure.map X P)

Tactic:
exact hX.isGaussian_map

Premises used: ProbabilityTheory.HasGaussianLaw.isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsGaussian μ
⊢ IsGaussian (mE := mE) (Measure.map id μ)

Tactic:
rwa [Measure.map_id]

Premises used: MeasureTheory.Measure.map_id
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
hX : HasGaussianLaw X P
⊢ AEMeasurable X P

Tactic:
AEMeasurable.of_map_ne_zero hX.isGaussian_map.toIsProbabilityMeasure.ne_zero

Premises used: AEMeasurable.of_map_ne_zero, MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
hX : HasGaussianLaw X P
⊢ IsProbabilityMeasure P

Tactic:
haveI := hX.isGaussian_map
    P.isProbabilityMeasure_of_map X

Premises used: MeasureTheory.Measure.isProbabilityMeasure_of_map
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
μ : Measure E
hX : HasLaw X μ P
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsGaussian μ
⊢ IsGaussian (mE := mE) (Measure.map X P)

Tactic:
rwa [hX.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
⊢ IsGaussian (mE := mE) (Measure.map X P)

Tactic:
have := hX.isGaussian_map
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
rw : IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))
hg : AEMeasurable.{u_2, u_5} (β := F) (_m := mE) (⇑L : (a : E) → F) (Measure.map X P)
hf : AEMeasurable X P
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map ((⇑L : (a : E) → F) ∘ X) P)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable]

Premises used: AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))

Tactic:
isGaussian_map_of_measurable hL

Premises used: ProbabilityTheory.isGaussian_map_of_measurable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
⊢ IsGaussian.{u_5} (E := F) (mE := inst_6) (Measure.map (⇑L : (a : E) → F) (Measure.map X P))

Tactic:
exact isGaussian_map_of_measurable hL

Premises used: ProbabilityTheory.isGaussian_map_of_measurable
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
⊢ AEMeasurable.{u_2, u_5} (β := F) (_m := mE) (⇑L : (a : E) → F) (Measure.map X P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid F
inst_5 : Module ℝ F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable.{u_2, u_5} (α := E) (β := F) (⇑L : (a : E) → F)
this : IsGaussian (mE := mE) (Measure.map X P)
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : Subsingleton E
inst_5 : IsProbabilityMeasure P
⊢ AEMeasurable X P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
Goal:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
X : Ω → E
inst_3 : NormedSpace ℝ E
inst_4 : Subsingleton E
inst_5 : IsProbabilityMeasure P
⊢ IsProbabilityMeasure (m0 := inst_1) (Measure.map X P)

Tactic:
have : IsProbabilityMeasure (P.map X) := P.isProbabilityMeasure_map (by fun_prop)