mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k ↦ f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε}

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
⊢ stoppedProcess u (σ ⊓ τ) = stoppedProcess u fun ω ↦ min (σ ω) (τ ω)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) → ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedAbove f i n ω) atTop (𝓝 c) := by
    rw [ae_all_iff]
    exact fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 hbdd)
  filter_upwards [ht] with ω hω hωb
  rw [BddAbove] at hωb
  obtain ⟨i, hi⟩ := exists_nat_gt hωb.some
  have hib : ∀ n, f n ω < i := by
    intro n
    exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi
  have heq : ∀ n, stoppedAbove f i n ω = f n ω := by
    intro n
    rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
    · simp only [le_top, inf_of_le_left]
      congr
    · simp [hib]
  simp only [← heq, hω i]

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
inst✝ : LinearOrder ι
i j : ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s μ
hij : i < j
⊢ (fun x ↦ μ.real (s j)) =ᵐ[μ] fun x ↦ μ.real (s j)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ω : Ω
hω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ |-f (i + 1) ω - -f i ω| ≤ ↑R

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ∞
this✝ : IsProbabilityMeasure μ
this :
  ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = (fun x ↦ μ.real (s (n + 1))) ω
ω : Ω
hω : ∀ (n : ℕ), μ[(s (n + 1)).indicator 1 | ↑(filtrationOfSet hsm) n] ω = μ.real (s (n + 1))
htends : ∀ (x : NNReal), ∀ᶠ (a : ℕ) in atTop, ↑x < ∑ k ∈ Finset.range a, μ (s (k + 1))
B : ℝ
hB : ∀ x ∈ Set.range fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1)), x ≤ B
n : ℕ
⊢ (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) n = ∑ a ∈ Finset.range n, (μ (s (a + 1))).toReal

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)) ↔ BddBelow (Set.range fun n ↦ f n ω)

Tactic:
← hω₂

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R
hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
ω : Ω
hω₁ : BddAbove (Set.range fun n ↦ f n ω) ↔ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
hω₂ : BddAbove (Set.range fun n ↦ (-f) n ω) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
this : (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ (-f) n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ (-f) n ω) ↔ BddBelow (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
by
  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

Goal state after:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ = (rexp (t * ε))⁻¹ * mgf X μ t

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
⊢ Integrable (stoppedValue u τ) μ

Tactic:
refine integrable_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_
  simp only [Finset.coe_Iic, Set.mem_image, Set.mem_Iic]
  specialize hbdd ω
  have h_top : τ ω ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
  lift τ ω to ι using h_top with i hi
  exact ⟨i, mod_cast hbdd, rfl⟩

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖

Tactic:
simp only [norm_eq_abs, abs_exp]
    conv_rhs => rw [abs_of_nonneg (by positivity)]
    -- ⊢ exp (t * |X ω| + v * X ω) ≤ exp ((v + t) * X ω) + exp ((v - t) * X ω)
    rcases le_total 0 (X ω) with h_nonneg | h_nonpos
    · rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]
      positivity
    · rw [abs_of_nonpos h_nonpos, mul_neg, mul_comm, ← mul_neg, mul_comm, ← add_mul, add_comm,
        ← sub_eq_add_neg, le_add_iff_nonneg_left]
      positivity

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ∞
inst✝ : AddCommGroup β
hle : τ ≤ π
N : ℕ
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hτ_top : ∀ (ω : Ω), τ ω ≠ ⊤
ω : Ω
i t : ℕ
ht : ↑t = τ ω
b : ℕ
hb : ↑b = π ω
hbdd : b ≤ N
⊢ t ≤ i → i < b → i ≤ N

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
h₁ : τ x = ↑n
h₂ : n + 1 ≤ n
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℂ
⊢ ∫ (x : Ω), cexp (t * ↑(id (X x))) ∂μ = complexMGF X μ t

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u

Tactic:
calc v + ((v - l) ⊓ (u - v)) / 2
    _ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
    _ ≤ v + (u - v) := by gcongr; exact inf_le_right
    _ = u := by abel

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ (deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      mgf X μ v ^ 2 =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
by
    rw [sub_div]
    congr 1
    · rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]
      exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
    · rw [deriv_cgf h]
      ring

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

Tactic:
let e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv

Goal state after:
case neg
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv
⊢ Measure.map (fun x ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map X μ =
    ∫ (v : ℝ), (BoundedContinuousFunction.char continuous_probChar ⋯ w) v ∂Measure.map Y μ'

Tactic:
simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
    RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ ∫ (v : ℝ), cexp (↑w * ↑v * I) ∂Measure.map X μ = ∫ (v : ℝ), cexp (↑w * ↑v * I) ∂Measure.map Y μ'
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case convert_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ContDiffOn ℝ (↑1 + 1) (cgf X μ) (Set.uIcc 0 t)

Tactic:
· rw [Set.uIcc_of_lt ht]
    exact (analyticOn_cgf.mono hs).contDiffOn hu

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
⊢ Var[⇑((toDualMap ℝ E) x); μ] = Var[fun u ↦ ⟪x, u⟫; μ]

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ cov[⇑((toDualMap ℝ E) x), ⇑((toDualMap ℝ E) y); μ] = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ : ℝ
v₁ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₁ v₁

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun u ↦ u.ofLp i) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω, (fun u ↦ u.ofLp j) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω; μ] =
    cov[X i, X j; μ]

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪(covarianceOperator μ) x, y⟫ =
    ⟪(continuousLinearMapOfBilin
          ((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
            (toDualMap ℝ E).toContinuousLinearMap))
        x,
      y⟫

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
this : IsGaussian (Measure.map ((fun x ↦ c + x) ∘ fun x ↦ -x) μ)
⊢ IsGaussian (Measure.map (fun x ↦ c + -x) μ)

Tactic:
Function.comp_def

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
this : IsGaussian (Measure.map (fun x ↦ c + -x) μ)
⊢ IsGaussian (Measure.map (fun x ↦ c + -x) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
h2 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E
h : Real.cos θ ^ 2 + Real.sin θ ^ 2 = 1
⊢ Real.cos θ ^ 2 * Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] -
          2 *
            (Real.cos θ *
              (Real.sin θ * cov[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E), ⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ])) +
        Real.sin θ ^ 2 * Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ] +
      (Real.sin θ ^ 2 * Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
          2 *
            (Real.sin θ *
              (Real.cos θ * cov[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E), ⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ])) +
        Real.cos θ ^ 2 * Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]) =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn : μ {x | normThreshold a n < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a}) ^ 2 ^ n
h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖} ≤ μ {x | normThreshold a n < ‖x‖} ^ 2
⊢ c⁻¹ * (c * ((1 - c) / c) ^ 2 ^ n) ^ 2 = c * ((1 - c) / c) ^ 2 ^ (n + 1)

Tactic:
by
      rw [mul_pow, ← pow_mul, ← mul_assoc, pow_two, ← mul_assoc,
        ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul, pow_add, pow_one]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsGaussian μ
t : E
⊢ cexp (↑⟪t, ∫ (x : E), x ∂μ⟫ * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑Var[fun u ↦ ⟪t, u⟫; μ] / 2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
⊢ (fun x ↦ ((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) (toLp 2 x)) =
    ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
h_le : ‖x‖ ^ 2 ≤ (1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2
⊢ C' * ((1 + ε) * ‖x - y‖ ^ 2 + (1 + 1 / ε) * ‖y‖ ^ 2) = C / ε * ‖y‖ ^ 2 + C * ‖x - y‖ ^ 2

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
hL_zero : μ (⇑L ⁻¹' {L x}) = 0
⊢ {x} ⊆ ⇑L ⁻¹' {L x}

Tactic:
exact fun ⦃a⦄ ↦ congrArg ⇑L

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ gaussianReal (∫ (x : Ω), id (X x) ∂P) Var[id ∘ X; P].toNNReal = gaussianReal (∫ (x : Ω), X x ∂P) Var[X; P].toNNReal

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), (fun x ↦ ⟪t, x⟫) (X x) ∂P) * I - ↑Var[(fun x ↦ ⟪t, x⟫) ∘ X; P] / 2) =
    cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
Function.comp_def

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), (fun x ↦ ⟪t, x⟫) (X x) ∂P) * I - ↑Var[fun x ↦ ⟪t, X x⟫; P] / 2) =
    cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
f g : (↥I → ℝ) → ℝ
⊢ cov[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm, g ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm;
      multivariateGaussian 0 (covMatrix I)] =
    cov[f ∘ ofLp, g ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm; multivariateGaussian 0 (covMatrix I)] =
    Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), L (X x) ∂P) * I - ↑Var[⇑L ∘ X; P] / 2) =
    cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)

Tactic:
Function.comp_def

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), L (X x) ∂P) * I - ↑Var[fun x ↦ L (X x); P] / 2) =
    cexp (↑(∫ (x : Ω), (fun x ↦ L (X x)) x ∂P) * I - ↑Var[fun x ↦ L (X x); P] / 2)