-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem tendsto_measure_of_le_liminf_measure_of_limsup_measure_le {ι : Type*} {L : Filter ι}
    {μ : Measure Ω} {μs : ι → Measure Ω} {E₀ E E₁ : Set Ω} (E₀_subset : E₀ ⊆ E) (subset_E₁ : E ⊆ E₁)
    (nulldiff : μ (E₁ \ E₀) = 0) (h_E₀ : μ E₀ ≤ L.liminf fun i ↦ μs i E₀)
    (h_E₁ : (L.limsup fun i ↦ μs i E₁) ≤ μ E₁) : L.Tendsto (fun i ↦ μs i E) (𝓝 (μ E))

Proof state:
case hinf
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ μ E ≤ liminf (fun i => (μs i) E) L

Tactic:
calc
  μ E = μ E₀ := measure_congr E₀_ae_eq_E.symm
  _ ≤ L.liminf fun i ↦ μs i E₀ := h_E₀
  _ ≤ L.liminf fun i ↦ μs i E :=
    liminf_le_liminf (.of_forall fun _ ↦ measure_mono E₀_subset)

Result:
no goals

Proof state:
case hinf
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ μ E ≤ liminf (fun i => (μs i) E) L

Tactic:
have E₀_ae_eq_E : E₀ =ᵐ[μ] E :=
  EventuallyLE.antisymm E₀_subset.eventuallyLE
    (subset_E₁.eventuallyLE.trans (ae_le_set.mpr nulldiff))

Result:
case hinf
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
E₀_ae_eq_E : E₀ =ᶠ[ae μ] E
⊢ μ E ≤ liminf (fun i => (μs i) E) L

Proof state:
case hsup
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ limsup (fun i => (μs i) E) L ≤ μ E

Tactic:
have E_ae_eq_E₁ : E =ᵐ[μ] E₁ :=
  EventuallyLE.antisymm subset_E₁.eventuallyLE
    ((ae_le_set.mpr nulldiff).trans E₀_subset.eventuallyLE)

Result:
case hsup
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ limsup (fun i => (μs i) E) L ≤ μ E

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ Tendsto (fun i => (μs i) E) L (𝓝 (μ E))

Tactic:
apply tendsto_of_le_liminf_of_limsup_le

Result:
case hinf
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ μ E ≤ liminf (fun i => (μs i) E) L

case hsup
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ limsup (fun i => (μs i) E) L ≤ μ E

case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => (μs i) E) _auto✝

case h'
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => (μs i) E) _auto✝

Proof state:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => (μs i) E) _auto✝

Tactic:
infer_param

Result:
no goals

Proof state:
case hsup
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
E_ae_eq_E₁ : E =ᶠ[ae μ] E₁
⊢ limsup (fun i => (μs i) E) L ≤ μ E

Tactic:
calc
  (L.limsup fun i ↦ μs i E) ≤ L.limsup fun i ↦ μs i E₁ :=
    limsup_le_limsup (.of_forall fun _ ↦ measure_mono subset_E₁)
  _ ≤ μ E₁ := h_E₁
  _ = μ E := measure_congr E_ae_eq_E₁.symm

Result:
no goals

Proof state:
case h'
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
E₀ E E₁ : Set Ω
E₀_subset : E₀ ⊆ E
subset_E₁ : E ⊆ E₁
nulldiff : μ (E₁ \ E₀) = 0
h_E₀ : μ E₀ ≤ liminf (fun i => (μs i) E₀) L
h_E₁ : limsup (fun i => (μs i) E₁) L ≤ μ E₁
⊢ autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => (μs i) E) _auto✝

Tactic:
infer_param

Result:
no goals