OAI/Analysis/Mahler/StripRegularLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.tendsto_strip_sublevel_mass line 13

   Source documentation

   Continuity from below, stated as convergence in the extended nonnegative reals.

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

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

2. theorem OAI.SymmetricMahler.manuscript_strip_regular_exhaustion line 24

   Source documentation

   The rank and exponent hypotheses yield an increasing regular exhaustion with compact boundaries, without a regular-value premise.

   theorem manuscript_strip_regular_exhaustion (A : J → I → ℝ)
       (hRank : Module.finrank ℝ (LinearMap.range (measurementLinear A)) = Fintype.card I)
       {m : ℕ} (hm : 2 ≤ 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)) ∧
       (∀ k, IsCompact {z | z ∈ stripDomain A ∧ stripTau A m z = stripRegularLevel k}) ∧
       (∀ k, frontier {z | z ∈ stripDomain A ∧ stripTau A m z < stripRegularLevel k} =
         {z | z ∈ stripDomain A ∧ stripTau A m z = stripRegularLevel k}) ∧
       (⋃ k, {z | z ∈ stripDomain A ∧ stripTau A m z < stripRegularLevel k}) =
   …

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