mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
contra : ¬0 ≤ δ / 2
⊢ (n + 1) • μ (closedBall 0 (δ / 2)) ≤ 0

Tactic:
suffices μ (closedBall 0 (δ / 2)) = 0 by simp [this]

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
contra : ¬0 ≤ δ / 2
⊢ μ (closedBall 0 (δ / 2)) = 0
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ X, f i b ≤ ⨆ y ∈ Y, f i y

Tactic:
intro x _

Goal state after:
case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
j✝ : x ∈ X
⊢ f x b ≤ ⨆ y ∈ Y, f x y
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
hx : x ∈ u
t : Set α
ht : t ∈ P
hxt : x ∈ t
⊢ P.Rel x x

Tactic:
exact ⟨t, ht, hxt, hxt⟩

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : SigmaFiniteFiltration μ ℱ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale (fun x ↦ f) ℱ μ

Tactic:
refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩
  rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
i j : ι
hij : i ≤ j
this : f i ≤ᵐ[μ.trim ⋯] μ[f j | ↑ℱ i]
⊢ f i ≤ᵐ[μ] μ[f j | ↑ℱ i]

Tactic:
by exact ae_le_of_ae_le_trim this

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
⊢ Martingale f 𝒢 μ

Tactic:
refine ⟨hadp, fun i j hij ↦ ?_⟩

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j : ℕ
hij : i ≤ j
⊢ μ[f j | ↑𝒢 i] =ᵐ[μ] f i
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  lowerCrossingTime a b f N k ω < N →
    upperCrossingTime a b f N k ω < N →
      upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
        lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
⊢ upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
    lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω

Tactic:
specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
      (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')

Goal state after:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
k : ℕ
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (k + 1) ω < N
h' : upperCrossingTime a b f N (k + 1) ω < N
⊢ upperCrossingTime a b f M (k + 1) ω = upperCrossingTime a b f N (k + 1) ω ∧
    lowerCrossingTime a b f M (k + 1) ω = lowerCrossingTime a b f N (k + 1) ω
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
h : ¬∃ j ∈ Set.Icc n m₁, u j ω ∈ s
j : ι
hj₁ : j ∈ Set.Icc n m₂
hj₂ : u j ω ∈ s
i : ι
hi₁ : i ∈ Set.Icc n m₂ ∩ {i | u i ω ∈ s}
hi₂ : i < m₁
⊢ False

Tactic:
exact h ⟨i, ⟨hi₁.1.1, hi₂.le⟩, hi₁.2⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
⊢ hτ.measurableSpace ≤ hπ.measurableSpace

Tactic:
refine fun s hs ↦ ⟨hs.1, fun i ↦ ?_⟩
  rw [(_ : s ∩ {ω | π ω ≤ i} = s ∩ {ω | τ ω ≤ i} ∩ {ω | π ω ≤ i})]
  · exact (hs.2 i).inter (hπ i)
  · ext
    simp only [Set.mem_inter_iff, iff_self_and, and_congr_left_iff, Set.mem_ofPred_eq]
    intro hle' _
    exact le_trans (hle _) hle'

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω ≤ ↑i}

Tactic:
refine ⟨le_iSup f i _ (hτ i), fun j ↦ ?_⟩
  have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by
    ext1 ω
    simp [Set.mem_inter_iff, Set.mem_ofPred_eq]
  rw [this]
  exact f.mono (min_le_right i j) _ (hτ _)

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
have hpi : IsPiSystem {s | ∃ n, MeasurableSet[ℱ n] s} := by
    rw [Set.ofPred_exists]
    exact isPiSystem_iUnion_of_monotone _ (fun n ↦ (ℱ n).isPiSystem_measurableSet) fun _ _ ↦ ℱ.mono

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ∞
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})

Tactic:
rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
    IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]
  refine ⟨fun h => ⟨h, ?_⟩, fun h ↦ h.1⟩
  have h' := h.2 i
  rwa [Set.inter_assoc, Set.inter_self] at h'

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : 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 : Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop

Tactic:
ENNReal.tendsto_nhds_top_iff_nnreal

Goal state after:
Ω : 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))
⊢ Tendsto (fun n ↦ ∑ x ∈ Finset.range n, μ.real (s (x + 1))) atTop atTop
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝ : AddCommMonoid E
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s
y : Ω
⊢ stoppedValue u τ y = (∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)) y

Tactic:
classical
  rw [stoppedValue, Finset.sum_apply, Finset.sum_indicator_eq_sum_filter]
  suffices {i ∈ s | y ∈ {ω : Ω | τ ω = (i : ι)}} = ({(τ y).untopA} : Finset ι) by
    rw [this, Finset.sum_singleton]
  ext1 ω
  simp only [Set.mem_ofPred_eq, Finset.mem_filter, Finset.mem_singleton]
  constructor <;> intro h
  · simp [h.2]
  · simp only [h]
    specialize hbdd y
    have : τ y ≠ ⊤ := fun h_contra ↦ by simp [h_contra] at hbdd
    lift τ y to ι using this with i hi
    simpa using hbdd

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ IsProbabilityMeasure (Measure.map X μ)

Tactic:
hX

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
hX : Measure.map X μ = Measure.dirac x
t : ℝ
⊢ IsProbabilityMeasure (Measure.dirac x)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inl
Ω : 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)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp ((t + v) * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
add_comm,

Goal state after:
case refine_2.inl
Ω : 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)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ rexp ((v + t) * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inr
Ω : 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)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp ((-t + v) * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
add_comm,

Goal state after:
case refine_2.inr
Ω : 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)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ rexp ((v + -t) * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | ↑n + 1 ≤ τ a}.indicator (u n) + {a | τ a = ↑n}.indicator (u n)) x

Tactic:
add_comm,

Goal state after:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x : Ω
⊢ {a | ↑n ≤ τ a}.indicator (u n) x = ({a | τ a = ↑n}.indicator (u n) + {a | ↑n + 1 ≤ τ a}.indicator (u n)) x
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖X a ^ p * rexp (v * X a)‖) μ

Tactic:
simp_rw [norm_eq_abs, abs_mul, abs_exp]
    have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg hp
    refine h.mono' ?_ ?_
    · fun_prop
    · refine ae_of_all _ fun ω ↦ ?_
      simp only [norm_mul, norm_eq_abs, abs_abs, abs_exp]
      gcongr
      exact abs_rpow_le_abs_rpow _ _

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (Measure.map X p)

Tactic:
hX

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (gaussianReal μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (Measure.map X p)

Tactic:
hX

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (gaussianReal μ v)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : 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)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * (t - 0) ^ 2 / 2

Tactic:
rw [← Set.uIoo_of_lt ht]

Goal state after:
Ω : 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)
⊢ ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * (t - 0) ^ 2 / 2
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ cgf X p t = μ * t + ↑v * t ^ 2 / 2

Tactic:
by
  rw [cgf, mgf_gaussianReal hX t, Real.log_exp]

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ ((covarianceBilin μ) x) x = x ^ 2 * Var[id; μ]

Tactic:
by
  rw [covarianceBilin_real, pow_two]

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

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map X P)

Tactic:
hX

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : eLpNorm id p μ ≠ ∞
⊢ ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top] at h

Goal state after:
case h₁
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : (∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≠ ∞
⊢ ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)

Tactic:
rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (id ∘ fun x ↦ x - ∫ (x : E), x ∂μ) 2 μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁

Tactic:
by_cases h : MemLp (fun x ↦ x - ∫ y, y ∂μ) 2 μ

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ ((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ ((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁
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 :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
⊢ ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ

Tactic:
filter_upwards [hC] with y hy

Goal state after:
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 :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable (fun y_1 ↦ rexp (C * ‖y + y_1‖ ^ 2)) (Measure.map (-id) μ)
⊢ Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s

Tactic:
add_comm,

Goal state after:
case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑t + ↑s - 2 * min ↑s ↑t = ↑t + ↑s - 2 * min ↑t ↑s
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : y ≤ ↑q - 1
h_le : ↑(qs y) ≤ ↑q - 1 + 1
⊢ qs y ≤ q

Tactic:
sub_add_cancel

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1
qs : ℝ → ℚ := fun x ↦ ⋯.choose
q : ℚ
y : ℝ
hy : y ≤ ↑q - 1
h_le : ↑(qs y) ≤ ↑q
⊢ qs y ≤ q
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s✝ s : Set (β × ℝ)
hs : s ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' s) ∂ν a = (κ a) s

Tactic:
rcases hs with ⟨t₁, ht₁, t₂, ht₂, rfl⟩
    simp only [mem_ofPred_eq] at ht₁ ht₂
    rw [← lintegral_add_compl _ ht₁]
    have h_eq1 : ∫⁻ x in t₁, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a)
        = ∫⁻ x in t₁, hf.toKernel f (a, x) t₂ ∂(ν a) := by
      refine setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)
      rw [mk_preimage_prod_right ha]
    have h_eq2 :
        ∫⁻ x in t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a) = 0 := by
      suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
      intro a hat₁
      rw [mem_compl_iff] at hat₁
      simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_empty]
    rw [h_eq1, h_eq2, add_zero]
    exact setLIntegral_toKernel_prod hf a ht₁ ht₂

Goal state after: