mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ∞
ε_pos' : ↑ε / 2 ≠ 0
⊢ limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F + ↑ε

Tactic:
let fs := F_closed.apprSeq

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
μs : ι → FiniteMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
F : Set Ω
F_closed : IsClosed[inst✝²] F
hne : L.NeBot
ε : ℝ≥0
ε_pos : 0 < ε
a✝ : ↑μ F < ∞
ε_pos' : ↑ε / 2 ≠ 0
fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq
⊢ limsup (fun i ↦ ↑(μs i) F) L ≤ ↑μ F + ↑ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s →
          μ s ≤ ENNReal.ofReal δ →
            eLpNorm (s.indicator ((fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε
    refine ⟨δ, hδ₁, fun n s hs hle => ?_⟩
    simp_rw [Finset.smul_sum, Finset.indicator_sum]
    refine le_trans (eLpNorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) ?_
    have this i : s.indicator ((n : ℝ)⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) :=
      indicator_const_smul _ _ _
    obtain rfl | hn := eq_or_ne n 0
    · simp
    simp_rw [this, eLpNorm_const_smul, ← Finset.mul_sum]
    rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]
    refine ENNReal.div_le_of_le_mul' ?_
    simpa using Finset.sum_le_card_nsmul (.range n) _ _ fun i _ => hδ₂ _ _ hs hle

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
ht1 : ∃ i, ∃ (_ : i ∈ u), t1 ∈ s i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rcases ht1 with ⟨n, hpn, ht1⟩

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_1
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ (fun ω ↦ AEMeasurable.mk X mX ω.1) =ᵐ[μ.prod ν] fun ω ↦ X ω.1

Tactic:
rw [← Function.comp_def, ← Function.comp_def]
    apply ae_eq_comp
    · exact measurable_fst.aemeasurable
    · rw [measurePreserving_fst.map_eq]
      exact (AEMeasurable.ae_eq_mk mX).symm

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) →
          ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (η a) (f i)) →
        (∀ i ∈ insert a s, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) →
          ∀ᵐ (a_3 : α) ∂μ, (η a_3) (⋂ i ∈ insert a s, f i) = ∏ i ∈ insert a s, (η a_3) (f i)

Tactic:
intro a S ha_notin_S h_rec hf_m

Goal state after:
case inr.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
⊢ ∀ᵐ (a_1 : α) ∂μ, (η a_1) (⋂ i ∈ insert a S, f i) = ∏ i ∈ insert a S, (η a_1) (f i)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ IndepSets {s | MeasurableSet s} {s} μ

Tactic:
apply indepSets_of_indepSets_of_le_right h_ind

Goal state after:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ {s} ⊆ {s | MeasurableSet s}
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
rw [← covariance_self, covariance_sum_left' (by simpa)]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ ∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ MemLp (∑ i ∈ s, X i) 2 μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ AEMeasurable (∑ i ∈ s, X i) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
i : ι
hi : i ∈ s
⊢ cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
covariance_sum_right' (by simpa) (hX i hi)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
i : ι
hi : i ∈ s
⊢ ∑ i_1 ∈ s, cov[X i, X i_1; μ] = ∑ j ∈ s, cov[X i, X j; μ]
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
hg : StronglyMeasurable g
⊢ ∃ h, StronglyMeasurable h ∧ g = h ∘ f

Tactic:
by
  let mX : MeasurableSpace X := mY.comap f
  induction g, hg using StronglyMeasurable.induction' with
  | const z => exact ⟨fun _ ↦ z, stronglyMeasurable_const, rfl⟩
  | @pcw g₁ g₂ s hg₁ hg₂ hs h₁ h₂ =>
    obtain ⟨t, ht, rfl⟩ := hs
    obtain ⟨h₁, mh₁, rfl⟩ := h₁
    obtain ⟨h₂, mh₂, rfl⟩ := h₂
    classical
    exact ⟨t.piecewise h₁ h₂, mh₁.piecewise ht mh₂, by rw [piecewise_comp]⟩
  | @lim g i hg hi h₁ h₂ =>
    choose h mh hh using h₁
    refine ⟨fun y ↦ limUnder atTop (h · y), StronglyMeasurable.limUnder mh, ?_⟩
    ext x
    rw [Function.comp_apply, Tendsto.limUnder_eq]
    simp_all

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
𝓕 : Filtration ι m
i : ι
hi : ∃ j > i, Set.Ioo i j = ∅
⊢ ↑𝓕₊ i = ↑𝓕 i

Tactic:
by
  let := Preorder.topology ι; have : OrderTopology ι := ⟨rfl⟩
  obtain ⟨j, hij, hIoo⟩ := hi
  have hcov : i ⋖ j := covBy_iff_Ioo_eq.mpr ⟨hij, hIoo⟩
  exact rightCont_eq_of_nhdsGT_eq_bot _ <| CovBy.nhdsGT hcov

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t} = MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_)

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ t ∈ {t | ∃ j ≤ i, s j = t}, MeasurableSet t

case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ t ∈ {s_1 | ∃ n, MeasurableSet s_1}, MeasurableSet t
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
⊢ MeasurableSet t

Tactic:
obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β n)

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t

case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t

case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t

case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ((s n).indicator fun x ↦ 1) ⁻¹' u = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ ‖f i‖ₑ ≤ eLpNorm f p count

Tactic:
calc
    ‖f i‖ₑ = eLpNorm f p (dirac i) := by rw [eLpNorm_dirac f i hp]
      _ = eLpNorm f p (count.restrict {i}) := by simp
      _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..

Goal state after:
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
⊢ ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ

Tactic:
induction n with

Goal state after:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
⊢ modularCharacterFun g = (map (fun x ↦ x * g) μ).haarScalarFactor μ

Tactic:
let ν := MeasureTheory.Measure.haar (G := G)

Goal state after:
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
⊢ modularCharacterFun g = (map (fun x ↦ x * g) μ).haarScalarFactor μ
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
mul_g_meas : Measurable fun x ↦ x * g
mul_h_meas : Measurable fun x ↦ x * h
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

Tactic:
let ν := MeasureTheory.Measure.haar (G := G)

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
mul_g_meas : Measurable fun x ↦ x * g
mul_h_meas : Measurable fun x ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have hgg' := hg'.aestronglyMeasurable.ae_eq_mk (μ := μ)

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᵐ[μ] AEStronglyMeasurable.mk g ⋯
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
⊢ (-f).nnrealPart = 0

Tactic:
by
  ext x
  simpa using hf x

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ CurveIntegrable ω γ

Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (curveIntegralFun ω γ) (Icc 0 1)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case hg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
inst✝ : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ 1 ⇑γ.extend I
hγs : ∀ (t : ↑I), γ t ∈ s
⊢ ContinuousOn (derivWithin ⇑γ.extend I) (Icc 0 1)

Tactic:
exact hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc a b), ‖deriv f x‖ ≤ B x

Tactic:
← uIoc_of_le hab

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (uIoc a b), ‖deriv f x‖ ≤ B x
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] fun x ↦ f x * g x
h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ
⊢ IntegrableOn f s ν

Tactic:
have h_Int : Integrable f ((μ.restrict s).withDensity ρ) := by
        rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] fun x ↦ f x * g x
h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
⊢ IntegrableOn f s ν
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ - c = torusMap 0 R θ

Tactic:
by
  ext1 i; simp [torusMap]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
⊢ univ.PairwiseDisjoint E

Tactic:
intro m _ n _ hmn

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
⊢ (Disjoint on E) m n
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
n : ℕ
⊢ invariants f ≤ invariants f^[n]

Tactic:
induction n with

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun N ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
B : Tendsto ((fun N ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 0)
⊢ ∃ N, 0 < N ∧ a' / ↑N * (b' + a' / ↑N) ≤ ε

Tactic:
obtain ⟨N, hN, h'N⟩ := (((tendsto_order.1 B).2 _ hε).and (Ici_mem_atTop 1)).exists

Goal state after:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun N ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
B : Tendsto ((fun N ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 0)
N : ℕ
hN : ((fun N ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) N < ε
h'N : 1 ≤ N
⊢ ∃ N, 0 < N ∧ a' / ↑N * (b' + a' / ↑N) ≤ ε