mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm ((s ∩ {x | C ≤ ‖f i x‖₊}).indicator (f i)) p μ + eLpNorm ((s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤
    eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ + ↑C * μ s ^ (1 / p.toReal)

Tactic:
refine add_le_add
        (eLpNorm_mono fun x => norm_indicator_le_of_subset Set.inter_subset_right _ _) ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm ((s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤ ↑C * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ ↑R

Tactic:
condExp_of_not_le hnm,

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |0 x| ≤ ↑R
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α), μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ

Tactic:
by
    refine integral_mono_of_nonneg ?_ integrable_condExp (Integrable.norm_condExp_rpow_le hp hf)
    filter_upwards with a using by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝¹⁰ : MeasurableSpace Ω
R : Type u_2
inst✝⁹ : SMul R ℝ≥0
inst✝⁸ : SMul R ℝ≥0∞
inst✝⁷ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝⁶ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝⁵ : TopologicalSpace Ω
inst✝⁴ : OpensMeasurableSpace Ω
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝² : PseudoMetricSpace R
inst✝¹ : Zero R
inst✝ : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

Tactic:
by
  simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, testAgainstNN_coe_eq,
    ENNReal.coe_smul]
  simp_rw [← smul_one_smul ℝ≥0∞ c (f _ : ℝ≥0∞), ← smul_one_smul ℝ≥0∞ c (lintegral _ _ : ℝ≥0∞),
    smul_eq_mul]
  exact lintegral_const_mul (c • (1 : ℝ≥0∞)) f.measurable_coe_ennreal_comp

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ, h⟩ := hg.eLpNorm_indicator_le le_rfl ENNReal.one_ne_top hε

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
⊢ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ Measure.map f '' S, μ Kᶜ ≤ ε

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
⊢ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ a ∈ S, (Measure.map f a) Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  ↑(2 * max M 1 * (δ⁻¹ ^ (1 / p.toReal) * δ ^ (1 / p.toReal))) ≤
    eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False

Tactic:
NNReal.inv_rpow,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
this :
  ↑(2 * max M 1 * ((δ ^ (1 / p.toReal))⁻¹ * δ ^ (1 / p.toReal))) ≤
    eLpNorm (f (ℐ (2 * max M 1 * (δ ^ (1 / p.toReal))⁻¹))) p μ
⊢ False
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω
hf : AEMeasurable f ↑μ
⊢ ↑μ (f ⁻¹' univ) ≤ ↑μ univ

Tactic:
exact measure_mono (subset_univ _)

Goal state after:
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
fs : ℕ → Ω →ᵇ ℝ≥0 := ⋯
key₁ : Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))
room₁ : ↑μ F < ↑μ F + ↑ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2
key₂ : Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))
room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near : ∀ᶠ (a : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs a) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2
⊢ ↑μ F + ↑ε / 2 + ↑ε / 2 ≤ ↑μ F + ↑ε

Tactic:
simp only [add_assoc, ENNReal.add_halves, le_refl]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ iIndepSets m κ μ

Tactic:
by
  rintro s f hf
  obtain rfl | ⟨i, rfl⟩ : s = ∅ ∨ ∃ i, s = {i} := by
    simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton
  all_goals simp

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ ↑C
⊢ ∃ C, ∀ (i : ↑{g | ∃ ni, TendstoInMeasure μ (fn ∘ ni) u g}), eLpNorm ((fun f ↦ ↑f) i) p μ ≤ ↑C

Tactic:
exact ⟨C, fun ⟨f, s, hs⟩ => eLpNorm_le_of_tendstoInMeasure
      (Eventually.of_forall fun n => hC (s n)) hs (fun n => hUI.1 (s n))⟩

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'
n : ι
hpn : n ∈ u
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact hyp n hpn t1 t2 ht1 ht2

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

Goal state before:
pp: case pos
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
A : Set α
hA : MeasurableSet A
hA' : X i ⁻¹' A = f i
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

Tactic:
exact .inter ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
          ⟨A ×ˢ Set.univ, hA.prod .univ, by ext; simp [← hA']⟩

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable (fun x ↦ (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (f ∘ X) ℙ

Tactic:
← integrable_map_measure (hf.mono_ac HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ),

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable (fun x ↦ (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable f (map X ℙ)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun k ↦ {s k}) S)

Tactic:
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

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

Goal state before:
pp: case inr.refine_4
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ IsPiSystem (piiUnionInter (fun k ↦ {s k}) T)

Tactic:
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] < ∞ → MemLp X 2 μ

Tactic:
contrapose!; rw [top_le_iff]; exact evariance_eq_top hX

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[c • Y, X; μ] = c * cov[X, Y; μ]

Tactic:
covariance_smul_left,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ c * cov[Y, X; μ] = c * cov[X, Y; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
⊢ (∫⁻ (a : Ω'), ‖X (Y a) - ∫ (x : Ω), X x ∂Measure.map (⇑Y) μ‖ₑ ^ 2 ∂μ).toReal =
    (∫⁻ (ω : Ω'), ‖(X ∘ ⇑Y) ω - ∫ (x : Ω'), (X ∘ ⇑Y) x ∂μ‖ₑ ^ 2 ∂μ).toReal

Tactic:
integral_map_equiv,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
⊢ (∫⁻ (a : Ω'), ‖X (Y a) - ∫ (x : Ω'), X (Y x) ∂μ‖ₑ ^ 2 ∂μ).toReal =
    (∫⁻ (ω : Ω'), ‖(X ∘ ⇑Y) ω - ∫ (x : Ω'), (X ∘ ⇑Y) x ∂μ‖ₑ ^ 2 ∂μ).toReal
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
· symm
    rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]
    refine ⟨?_, ENNReal.ofReal_ne_top⟩
    rw [MemLp, not_and] at hℒ
    specialize hℒ hX
    simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, not_lt,
      top_le_iff, ENNReal.toReal_ofNat, one_div, ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos,
      and_true, or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ
    exact mod_cast hℒ fun _ => zero_le_two

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
⊢ ∫ (ω : Ω),
      (X ω - ∫ (x : Ω), X x ∂Measure.map (⇑Z) μ) * (Y ω - ∫ (x : Ω), Y x ∂Measure.map (⇑Z) μ) ∂Measure.map (⇑Z) μ =
    ∫ (ω : Ω'), ((X ∘ ⇑Z) ω - ∫ (x : Ω'), (X ∘ ⇑Z) x ∂μ) * ((Y ∘ ⇑Z) ω - ∫ (x : Ω'), (Y ∘ ⇑Z) x ∂μ) ∂μ

Tactic:
integral_map_equiv,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
⊢ ∫ (x : Ω'), (X (Z x) - ∫ (x : Ω'), X (Z x) ∂μ) * (Y (Z x) - ∫ (x : Ω'), Y (Z x) ∂μ) ∂μ =
    ∫ (ω : Ω'), ((X ∘ ⇑Z) ω - ∫ (x : Ω'), (X ∘ ⇑Z) x ∂μ) * ((Y ∘ ⇑Z) ω - ∫ (x : Ω'), (Y ∘ ⇑Z) x ∂μ) ∂μ
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν

Tactic:
have A : AEStronglyMeasurable id (Measure.map f μ) := by
      rw [aestronglyMeasurable_iff_aemeasurable_separable]
      rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
      refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
      rw [ae_map_iff h.aemeasurable_fst]
      · filter_upwards [ht] with x hx using subset_closure hx
      · exact isClosed_closure.measurableSet
    change ∫ x, id (f x) ∂μ = ∫ x, id (g x) ∂ν
    rw [← integral_map h.aemeasurable_fst A]
    rw [h.map_eq] at A
    rw [← integral_map h.aemeasurable_snd A, h.map_eq]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) κ μ

Tactic:
by
  have h : IndepFun (fun a ↦ ((hf_meas i).mk (f i) a, (hf_meas j).mk (f j) a))
      (fun a ↦ ((hf_meas k).mk (f k) a, (hf_meas l).mk (f l) a)) κ μ := by
    refine iIndepFun.indepFun_prodMk_prodMk ?_ (fun i ↦ (hf_meas i).measurable_mk) _ _ _ _ hik hil
      hjk hjl
    exact iIndepFun.congr' hf_indep fun i ↦ Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk
  refine IndepFun.congr' h ?_ ?_
  · filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas j).ae_eq_mk] with a hi hj
    filter_upwards [hi, hj] with ω hωi hωj
    rw [← hωi, ← hωj]
  · filter_upwards [Measure.ae_ae_of_ae_comp (hf_meas k).ae_eq_mk,
      Measure.ae_ae_of_ae_comp (hf_meas l).ae_eq_mk] with a hk hl
    filter_upwards [hk, hl] with ω hωk hωl
    rw [← hωk, ← hωl]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ eLpNormEssSup ((⋂ n ∈ u, s n).indicator 1) μ < ↑‖1 x‖₊

Tactic:
eLpNormEssSup_eq_zero_iff.2

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ 0 < ↑‖1 x‖₊

α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ (⋂ n ∈ u, s n).indicator 1 =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ μ (s ∩ F i ∪ t ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)

Tactic:
measure_union (hdisj.inter_left _ |>.inter_right _) (ht.inter hi),

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ (μ (s ∩ F i) + μ (t ∩ F i)) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)
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
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

Tactic:
have mul_h_meas : Measurable (· * h) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) h

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
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g f : α →C_c β
⊢ HasCompactSupport (-⇑f.toContinuousMap)

Tactic:
simpa [HasCompactSupport, tsupport] using f.2

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

Tactic:
apply (f₁.hasCompactSupport'.union f₂.hasCompactSupport').of_isClosed_subset isClosed_closure
    rw [tsupport, tsupport, ← closure_union]
    apply closure_mono
    intro x hx
    contrapose hx
    simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, Set.mem_union, Function.mem_support,
      ne_eq, not_or, Decidable.not_not, ContinuousMap.coe_sub, Pi.sub_apply] at hx ⊢
    simp [hx.1, hx.2]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case neg
α : 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
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
have hν0' : (ν s).toReal ≠ 0 := by simpa using! hν0
    have hνfin : ν s ≠ ⊤ := by intro this; apply hν0'; simp [this]
    have hν0'' : ν s ≠ 0 := by intro this; apply hν0'; simp [this]
    have hint : IntegrableOn f s ν := by
      have hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] (fun x ↦ f x * g x) := by
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      have h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ := by
        rwa [integrableOn_congr_fun_ae hmul_ae]
      have h_Int : Integrable f ((μ.restrict s).withDensity ρ) := by
        rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]
      have hνrs : ν.restrict s = (μ.restrict s).withDensity ρ := by
        ext t ht
        simp [ht, ν, hs_meas]
      simpa [IntegrableOn, hνrs] using! h_Int
    obtain ⟨c, hc, h_ave⟩ := exists_eq_setAverage hs_conn hf hint hνfin hν0''
    refine ⟨c, hc, ?_⟩
    calc
      _ = ∫ x in s, f x ∂ν := heq
      _ = f c * ∫ x in s, (1 : ℝ) ∂ν := by
        rw [h_ave]
        simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]
        rw [measureReal_def]
        field_simp
      _ = _ := by simp [hg1]

Goal state after: