Sections.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.AffineSlice.fiber line 16
Source documentation
A vertical affine section of a set in a product vector space.
```
def fiber (K : Set (U × V)) (p : U) : Set V := (fun y => (p, y)) ⁻¹' K
…
```
theorem OAI.Problem358.AffineSlice.isClosed_fiber line 19
theorem OAI.Problem358.AffineSlice.fiber_subset_projection line 23
theorem OAI.Problem358.AffineSlice.isCompact_fiber line 27
theorem OAI.Problem358.AffineSlice.continuousAt_fiberMeasure line 37
Source documentation
Fiber volume is continuous at every prefix whose fiber crosses the interior. This supplies the density-continuity step of triangular uniform parametrization.
```
theorem continuousAt_fiberMeasure {K : Set (U × V)} (hK : IsCompact K)
    (hconv : Convex ℝ K) {p : U} (hp : ∃ y : V, (p, y) ∈ interior K) :
    ContinuousAt (fun q => μ (fiber K q)) p := by
…
```
Mentions: OAI.Problem358.AffineSlice.fiber

theorem OAI.Problem358.AffineSlice.continuousAt_fiberMeasureReal line 66

Source documentation

The same slice-volume continuity in real, rather than extended-real, values.

theorem continuousAt_fiberMeasureReal {K : Set (U × V)} (hK : IsCompact K)
    (hconv : Convex ℝ K) {p : U} (hp : ∃ y : V, (p, y) ∈ interior K) :
    ContinuousAt (fun q => μ.real (fiber K q)) p := by
…

Mentions: OAI.Problem358.AffineSlice.fiber

theorem OAI.Problem358.AffineSlice.fiberMeasure_pos line 75
Source documentation
A fiber crossing the interior has positive volume.
```
theorem fiberMeasure_pos {K : Set (U × V)} {p : U}
    (hp : ∃ y : V, (p, y) ∈ interior K) : 0 < μ (fiber K p) := by
…
```
Mentions: OAI.Problem358.AffineSlice.fiber
theorem OAI.Problem358.AffineSlice.fiberMeasureReal_pos line 85
Source documentation
Positivity survives conversion to real for compact fibers.
```
theorem fiberMeasureReal_pos {K : Set (U × V)} (hK : IsCompact K) {p : U}
    (hp : ∃ y : V, (p, y) ∈ interior K) : 0 < μ.real (fiber K p) := by
…
```
Mentions: OAI.Problem358.AffineSlice.fiber
def OAI.Problem358.SectionMeasure.fiber line 103
Source documentation
The fiber of a product set over its first coordinate.
```
def fiber {A B : Type*} (U : Set (A × B)) (a : A) : Set B :=
…
```
theorem OAI.Problem358.SectionMeasure.fiber_nonempty_iff line 107
Source documentation
A fiber is nonempty exactly when its prefix belongs to the projection.
```
theorem fiber_nonempty_iff {A B : Type*} (U : Set (A × B)) (a : A) :
    (fiber U a).Nonempty ↔ a ∈ Prod.fst '' U := by
…
```
Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.isOpen_fiber line 118

Source documentation

Fibers of open sets are open.

theorem isOpen_fiber {A B : Type*} [TopologicalSpace A] [TopologicalSpace B]
    {U : Set (A × B)} (hU : IsOpen U) (a : A) : IsOpen (fiber U a) :=
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.isOpen_projection line 123

Source documentation

Prefix domains of open sets are open.

theorem isOpen_projection {A B : Type*} [TopologicalSpace A] [TopologicalSpace B]
    {U : Set (A × B)} (hU : IsOpen U) : IsOpen (Prod.fst '' U) :=
…

theorem OAI.Problem358.SectionMeasure.fiber_measure_pos_iff line 128

Source documentation

Open fibers have positive mass exactly on the prefix domain.

theorem fiber_measure_pos_iff {A B : Type*}
    [TopologicalSpace A] [TopologicalSpace B] [MeasurableSpace B]
    (ν : Measure B) [Measure.IsOpenPosMeasure ν]
    {U : Set (A × B)} (hU : IsOpen U) (a : A) :
    0 < ν (fiber U a) ↔ a ∈ Prod.fst '' U := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.fiber_measure_ne_top_of_subset_compact line 136

Source documentation

A compact ambient envelope bounds every fiber by the same compact projection.

theorem fiber_measure_ne_top_of_subset_compact {A B : Type*}
    [TopologicalSpace A] [TopologicalSpace B] [MeasurableSpace B]
    (ν : Measure B) [IsFiniteMeasureOnCompacts ν]
    {U K : Set (A × B)} (hK : IsCompact K) (hUK : U ⊆ K) (a : A) :
    ν (fiber U a) ≠ ∞ := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.fiber_measure_toReal_pos line 147

Source documentation

Conditional section densities are strictly positive and finite on the prefix domain.

theorem fiber_measure_toReal_pos {A B : Type*}
    [TopologicalSpace A] [TopologicalSpace B] [MeasurableSpace B]
    (ν : Measure B) [Measure.IsOpenPosMeasure ν] [IsFiniteMeasureOnCompacts ν]
    {U K : Set (A × B)} (hU : IsOpen U) (hK : IsCompact K) (hUK : U ⊆ K)
    {a : A} (ha : a ∈ Prod.fst '' U) :
    0 < (ν (fiber U a)).toReal := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.convex_fiber line 157

Source documentation

Every fiber of a convex product set is convex.

theorem convex_fiber {A B : Type*} [AddCommMonoid A] [AddCommMonoid B]
    [Module ℝ A] [Module ℝ B] {U : Set (A × B)} (hU : Convex ℝ U) (a : A) :
    Convex ℝ (fiber U a) := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.convex_projection line 165

Source documentation

Projecting a convex product set preserves convexity.

theorem convex_projection {A B : Type*} [AddCommMonoid A] [AddCommMonoid B]
    [Module ℝ A] [Module ℝ B] {U : Set (A × B)} (hU : Convex ℝ U) :
    Convex ℝ (Prod.fst '' U) :=
…

theorem OAI.Problem358.SectionMeasure.eq_Ioo_csInf_csSup_of_open_convex line 171

Source documentation

A nonempty bounded open convex subset of the real line is its endpoint interval.

theorem eq_Ioo_csInf_csSup_of_open_convex {S : Set ℝ}
    (hS : IsOpen S) (hc : Convex ℝ S) (hne : S.Nonempty)
    (hl : BddBelow S) (hu : BddAbove S) :
    S = Ioo (sInf S) (sSup S) := by
…

theorem OAI.Problem358.SectionMeasure.exists_fiber_eq_Ioo line 193

Source documentation

Nonempty scalar fibers of a bounded open convex set are bounded open intervals.

theorem exists_fiber_eq_Ioo {A : Type*} [TopologicalSpace A]
    [AddCommMonoid A] [Module ℝ A]
    {U K : Set (A × ℝ)} (hU : IsOpen U) (hc : Convex ℝ U)
    (hK : IsCompact K) (hUK : U ⊆ K) {a : A} (ha : a ∈ Prod.fst '' U) :
    ∃ l r : ℝ, l < r ∧ fiber U a = Ioo l r := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.measurable_fiber_measure line 211

Source documentation

Section volume is a measurable function of its prefix.

theorem measurable_fiber_measure {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U) :
    Measurable (fun a => ν (fiber U a)) :=
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.measurable_fiber_measure_toReal line 217
Source documentation
Real-valued section volume is measurable, including the zero extension outside the projection.
```
theorem measurable_fiber_measure_toReal {A B : Type*}
    [MeasurableSpace A] [MeasurableSpace B]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U) :
    Measurable (fun a => (ν (fiber U a)).toReal) :=
…
```
Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.lintegral_fiber_measure line 224

Source documentation

Tonelli's recursion for section volumes.

theorem lintegral_fiber_measure {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) (ν : Measure B) [SFinite ν]
    {U : Set (A × B)} (hU : MeasurableSet U) :
    (∫⁻ a, ν (fiber U a) ∂μ) = (μ.prod ν) U :=
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.integral_fiber_measure_toReal line 231

Source documentation

Finite section mass gives the real-valued recursion used by conditional densities.

theorem integral_fiber_measure_toReal {A B : Type*}
    [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) (ν : Measure B) [SFinite ν]
    {U : Set (A × B)} (hU : MeasurableSet U) (hfin : (μ.prod ν) U ≠ ∞) :
    (∫ a, (ν (fiber U a)).toReal ∂μ) = ((μ.prod ν) U).toReal := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.integral_normalized_fiber_measure line 241

Source documentation

A positive finite section mass normalizes its conditional section density to one.

theorem integral_normalized_fiber_measure {A B : Type*}
    [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) (ν : Measure B) [SFinite ν]
    {U : Set (A × B)} (hU : MeasurableSet U) (hfin : (μ.prod ν) U ≠ ∞)
    (hpos : 0 < ((μ.prod ν) U).toReal) :
    (∫ a, (ν (fiber U a)).toReal / ((μ.prod ν) U).toReal ∂μ) = 1 := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMarginal.map_fst_withDensity line 259

Source documentation

Integrating a product density over the second coordinate computes its actual first marginal.

theorem map_fst_withDensity (q : A × B → ℝ≥0∞) (hq : Measurable q) :
    Measure.map Prod.fst ((μ.prod ν).withDensity q) =
      μ.withDensity (fun a => ∫⁻ b, q (a, b) ∂ν) := by
…

theorem OAI.Problem358.SectionMarginal.map_fst_restrict line 275
Source documentation
A body restricted from a product measure has section-volume density in its first marginal. This remains valid for zero and infinite total body measure.
```
theorem map_fst_restrict (U : Set (A × B)) (hU : MeasurableSet U) :
    Measure.map Prod.fst ((μ.prod ν).restrict U) =
      μ.withDensity (fun a => ν {b | (a, b) ∈ U}) := by
…
```

theorem OAI.Problem358.SectionMarginal.map_fst_normalized_restrict line 292

Source documentation

The normalized body law has the common total-volume normalization, rather than a separate normalization of each prefix.

theorem map_fst_normalized_restrict (U : Set (A × B)) (hU : MeasurableSet U) :
    Measure.map Prod.fst (((μ.prod ν) U)⁻¹ • (μ.prod ν).restrict U) =
      ((μ.prod ν) U)⁻¹ • μ.withDensity (fun a => ν {b | (a, b) ∈ U}) := by
…

theorem OAI.Problem358.SectionMarginal.lintegral_sections line 298

Source documentation

Section masses integrate to the total body mass.

theorem lintegral_sections (U : Set (A × B)) (hU : MeasurableSet U) :
    (∫⁻ a, ν {b | (a, b) ∈ U} ∂μ) = (μ.prod ν) U :=
…

def OAI.Problem358.SectionMass.mass line 314

Source documentation

The mass of a vertical section of a set.

def mass {X Y : Type*} [MeasurableSpace Y]
    (ν : Measure Y) (U : Set (X × Y)) (x : X) : ℝ≥0∞ :=
…

lemma OAI.Problem358.SectionMass.measurable_mass line 318
lemma OAI.Problem358.SectionMass.measurable_mass_toReal line 323
lemma OAI.Problem358.SectionMass.positive_iff_mem_projection line 328
lemma OAI.Problem358.SectionMass.isOpen_positive_mass line 341

lemma OAI.Problem358.SectionMass.isCompact_fiber line 352

Source documentation

Compact ambient sets have compact vertical sections, in arbitrary factors.

lemma isCompact_fiber {X Y : Type*}
    [TopologicalSpace X] [T2Space X] [TopologicalSpace Y]
    {K : Set (X × Y)} (hK : IsCompact K) (x : X) :
    IsCompact (Prod.mk x ⁻¹' K) := by
…

lemma OAI.Problem358.SectionMass.mass_lt_top_of_compact line 370

lemma OAI.Problem358.SectionMass.interior_mass_pos_lt_top line 379

Source documentation

On the projection of the interior of a compact body, its section density is strictly positive and finite. These are the denominators of conditional densities.

lemma interior_mass_pos_lt_top {X Y : Type*}
    [TopologicalSpace X] [T2Space X] [TopologicalSpace Y]
    [MeasurableSpace Y] (ν : Measure Y)
    [Measure.IsOpenPosMeasure ν] [IsLocallyFiniteMeasure ν]
    {K : Set (X × Y)} (hK : IsCompact K) {x : X}
    (hx : x ∈ Prod.fst '' interior K) :
    0 < mass ν (interior K) x ∧
      mass ν (interior K) x ≤ mass ν K x ∧ mass ν K x < ∞ := by
…

Mentions: OAI.Problem358.SectionMass.mass

lemma OAI.Problem358.SectionMass.convex_positive_mass line 392

Source documentation

The positivity domain of section masses of an open convex set is convex.

lemma convex_positive_mass {X Y : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasurableSpace Y]
    (ν : Measure Y) [Measure.IsOpenPosMeasure ν]
    {U : Set (X × Y)} (hU : IsOpen U) (hc : Convex ℝ U) :
    Convex ℝ {x | 0 < mass ν U x} := by
…

Mentions: OAI.Problem358.SectionMass.mass

lemma OAI.Problem358.SectionMass.mass_prod line 405

Source documentation

Successive section masses satisfy the exact Tonelli recursion.

lemma mass_prod {X Y Z : Type*}
    [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
    (ν : Measure Y) (ρ : Measure Z) [SFinite ρ]
    {U : Set (X × (Y × Z))} (hU : MeasurableSet U) (x : X) :
    mass (ν.prod ρ) U x =
      ∫⁻ y, ρ {z | (x, (y, z)) ∈ U} ∂ν := by
…

Mentions: OAI.Problem358.SectionMass.mass

lemma OAI.Problem358.SectionMass.interior_mass_toReal_pos line 413
theorem OAI.Problem358.SectionMeasure.upperSemicontinuous_fiber_inf line 434
Source documentation
The lower endpoint of a nonempty open scalar fiber is upper semicontinuous in its prefix. No convexity is needed for this regularity statement.
```
theorem upperSemicontinuous_fiber_inf {A : Type*} [TopologicalSpace A]
    {U : Set (A × ℝ)} (hU : IsOpen U)
    (hb : ∀ a ∈ Prod.fst '' U, BddBelow (fiber U a)) :
    UpperSemicontinuous (fun a : Prod.fst '' U => sInf (fiber U a.val)) := by
…
```
Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.lowerSemicontinuous_fiber_sup line 458

Source documentation

The upper endpoint is lower semicontinuous on the valid-prefix domain.

theorem lowerSemicontinuous_fiber_sup {A : Type*} [TopologicalSpace A]
    {U : Set (A × ℝ)} (hU : IsOpen U)
    (hb : ∀ a ∈ Prod.fst '' U, BddAbove (fiber U a)) :
    LowerSemicontinuous (fun a : Prod.fst '' U => sSup (fiber U a.val)) := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.measurable_fiber_inf line 482

Source documentation

Lower scalar-section endpoints are Borel functions of their valid prefix.

theorem measurable_fiber_inf {A : Type*} [TopologicalSpace A]
    [MeasurableSpace A] [OpensMeasurableSpace A]
    {U : Set (A × ℝ)} (hU : IsOpen U)
    (hb : ∀ a ∈ Prod.fst '' U, BddBelow (fiber U a)) :
    Measurable (fun a : Prod.fst '' U => sInf (fiber U a.val)) :=
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.measurable_fiber_sup line 490

Source documentation

Upper scalar-section endpoints are Borel functions of their valid prefix.

theorem measurable_fiber_sup {A : Type*} [TopologicalSpace A]
    [MeasurableSpace A] [OpensMeasurableSpace A]
    {U : Set (A × ℝ)} (hU : IsOpen U)
    (hb : ∀ a ∈ Prod.fst '' U, BddAbove (fiber U a)) :
    Measurable (fun a : Prod.fst '' U => sSup (fiber U a.val)) :=
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.exists_measurable_fiber_endpoints line 499

Source documentation

A bounded open convex region has a measurably varying interval description of all of its nonempty scalar sections.

theorem exists_measurable_fiber_endpoints {A : Type*} [TopologicalSpace A]
    [MeasurableSpace A] [OpensMeasurableSpace A]
    [AddCommMonoid A] [Module ℝ A]
    {U K : Set (A × ℝ)} (hU : IsOpen U) (hc : Convex ℝ U)
    (hK : IsCompact K) (hUK : U ⊆ K) :
    ∃ l r : (Prod.fst '' U) → ℝ, Measurable l ∧ Measurable r ∧
      ∀ a, l a < r a ∧ fiber U a.val = Ioo (l a) (r a) := by
…

Mentions: OAI.Problem358.SectionMeasure.fiber

theorem OAI.Problem358.SectionMeasure.exists_measurable_projected_fiber_endpoints line 525

Source documentation

The scalar projection of each remaining multidimensional section has measurable interval endpoints. This is the support interval for conditional quantiles.

theorem exists_measurable_projected_fiber_endpoints {A B : Type*}
    [TopologicalSpace A] [TopologicalSpace B]
    [MeasurableSpace A] [OpensMeasurableSpace A]
    [AddCommMonoid A] [Module ℝ A] [AddCommMonoid B] [Module ℝ B]
    {U K : Set ((A × ℝ) × B)} (hU : IsOpen U) (hc : Convex ℝ U)
    (hK : IsCompact K) (hUK : U ⊆ K) :
    ∃ l r : (Prod.fst '' (Prod.fst '' U)) → ℝ,
      Measurable l ∧ Measurable r ∧ ∀ a,
        l a < r a ∧ {t | ∃ b, ((a.val, t), b) ∈ U} = Ioo (l a) (r a) := by
…