OAI/Analysis/AffineBernstein/FiniteAreaCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.integral_le_sum_cover line 20

   Source comment

   Subadditivity for a finite (not disjoint) measurable cover, including the nonintegrable convention for the left-hand Bochner integral.

   lemma integral_le_sum_cover {X ι : Type*} [MeasurableSpace X] [Fintype ι]
       {μ : Measure X} {K : Set X} {S : ι → Set X} {f : X → ℝ}
       (hK : MeasurableSet K) (hS : ∀ i, MeasurableSet (S i))
       (hsub : ∀ i, S i ⊆ K) (hcover : K ⊆ ⋃ i, S i)
       (hn : ∀ x ∈ K, 0 ≤ f x) :
       (∫ x in K, f x ∂μ) ≤ ∑ i, ∫ x in S i, f x ∂μ := by
   …

2. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normed_compact_interior line 55

   Source comment

   Compact inner containment in the actual interiors of the approximants.

   theorem LocalDistanceConverges.eventually_normed_compact_interior
       {Cj : ℕ → Set E} {C S : Set E} (h : LocalDistanceConverges Cj C)
       (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
       (hnej : ∀ j, (Cj j).Nonempty) (hS : IsCompact S)
       (hSC : S ⊆ interior C) : ∀ᶠ j in atTop, S ⊆ interior (Cj j) := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges