OAI/Analysis/Mahler/StripMassExhaustion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.stripRegularLevel line 15
2. lemma OAI.SymmetricMahler.stripRegularLevel_mem line 17
3. lemma OAI.SymmetricMahler.strictMono_stripRegularLevel line 22
4. lemma OAI.SymmetricMahler.tendsto_stripRegularLevel line 29
5. theorem OAI.SymmetricMahler.strip_regular_value_sequence line 36

   Source documentation

   Explicit sequence for the actual tau, with no regular-value premise.

   theorem strip_regular_value_sequence (A : J → I → ℝ)
       (hA : Function.Injective (measurement A)) {m : ℕ} (hm : 0 < m) :
       StrictMono stripRegularLevel ∧
       (∀ k, stripRegularLevel k ∈ Ioo (0 : ℝ) 1) ∧
       Tendsto stripRegularLevel atTop (𝓝 1) ∧
       ∀ k z, z ∈ stripDomain A → stripTau A m z = stripRegularLevel k →
         Function.Surjective (fderiv ℝ (stripTau A m) z) := by
   …

   Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.stripRegularLevel, OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau

6. lemma OAI.SymmetricMahler.strip_regular_sublevels_monotone line 46
7. lemma OAI.SymmetricMahler.strip_regular_sublevels_union line 51
8. theorem OAI.SymmetricMahler.strip_mass_exhaustion_iSup line 67

   Source documentation

   Continuity from below of nonnegative mass on the actual sublevels. No finiteness of the mass over the limiting open set is imposed.

   theorem strip_mass_exhaustion_iSup (A : J → I → ℝ) (m : ℕ)
       (μ : Measure ((I → ℝ) × (I → ℝ))) (ρ : ((I → ℝ) × (I → ℝ)) → ℝ≥0∞) :
       (∫⁻ z in {z | z ∈ stripDomain A ∧ stripTau A m z < 1}, ρ z ∂μ) =
         ⨆ k, ∫⁻ z in {z | z ∈ stripDomain A ∧ stripTau A m z < stripRegularLevel k}, ρ z ∂μ := by
   …

   Mentions: OAI.SymmetricMahler.stripDomain, OAI.SymmetricMahler.stripTau, OAI.SymmetricMahler.stripRegularLevel