LeanPool.SardMoreira.MeasureBallSemicontinuous #
theorem
MeasureTheory.tendsto_measure_biUnion_lt
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ι : Type u_2}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
{s : ι → Set α}
{a : ι}
(hm : ∀ (i j : ι), i ≤ j → j < a → s i ⊆ s j)
:
Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Iio a)) (nhds (μ (⋃ (i : ι), ⋃ (_ : i < a), s i)))
theorem
continuousWithinAt_Iio_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
{x✝ : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
{x : X}
{r : ℝ}
:
ContinuousWithinAt (fun (x_1 : ℝ) => μ (Metric.ball x x_1)) (Set.Iio r) r
theorem
continuousWithinAt_Iic_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
{x✝ : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
{x : X}
{r : ℝ}
:
ContinuousWithinAt (fun (x_1 : ℝ) => μ (Metric.ball x x_1)) (Set.Iic r) r
theorem
lowerSemicontinuous_measure_ball_toUpper_symm
{X : Type u_1}
[PseudoMetricSpace X]
{x✝ : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
:
LowerSemicontinuous fun (xr : X × Topology.WithUpper ℝ) => μ (Metric.ball xr.1 (Topology.WithUpper.toUpper.symm xr.2))
theorem
lowerSemicontinuous_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
{x✝ : MeasurableSpace X}
{μ : MeasureTheory.Measure X}
:
LowerSemicontinuous fun (xr : X × ℝ) => μ (Metric.ball xr.1 xr.2)
theorem
Measurable.measure_ball
{α : Type u_1}
{X : Type u_2}
{x✝ : MeasurableSpace α}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
{f : α → X}
{g : α → ℝ}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (a : α) => μ (Metric.ball (f a) (g a))
theorem
IsCompact.exists_isMinOn_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X)
{s : Set X}
(hs : IsCompact s)
(hne : s.Nonempty)
(r : ℝ)
:
∃ x ∈ s, IsMinOn (fun (x : X) => μ (Metric.ball x r)) s x
theorem
IsCompact.exists_pos_forall_lt_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X)
[μ.IsOpenPosMeasure]
{s : Set X}
(hs : IsCompact s)
{r : ℝ}
(hr : 0 < r)
:
∃ m > 0, ∀ x ∈ s, ↑m < μ (Metric.ball x r)
theorem
exists_pos_forall_lt_measure_ball
{X : Type u_1}
[PseudoMetricSpace X]
[CompactSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X)
[μ.IsOpenPosMeasure]
{r : ℝ}
(hr : 0 < r)
:
∃ m > 0, ∀ (x : X), ↑m < μ (Metric.ball x r)