OAI/MathematicalPhysics/Boltzmann/Branching/SubmersionNullPreimage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.GainPullback.exists_complementary_chart line 22
2. theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_surjective_pullback_zero line 67

   Source documentation

   The L1 form of the manuscript's uniform pullback estimate.

   theorem compact_surjective_pullback_zero {O K Z : Set E} (hO : IsOpen O)
       (hK : IsCompact K) (hKO : K ⊆ O) (hZ : ((volume : Measure P).prod volume) Z = 0)
       {Φ : ℕ → E → P} {Φ' : ℕ → E → E →L[ℝ] P} {φ' : E → E →L[ℝ] P}
       (hder : ∀ n, ∀ x ∈ O, HasFDerivAt (Φ n) (Φ' n x) x)
       (hcont : ∀ x ∈ O, ContinuousAt φ' x)
       (hreg : ∀ x ∈ K \ Z, Surjective (φ' x))
       (hconv : ∀ x ∈ O, ∀ r > 0, ball x r ⊆ O →
         TendstoUniformlyOn Φ' φ' atTop (ball x r))
       {g : ℕ → P → ℝ≥0∞} {ρ : ℕ → E → ℝ≥0∞} {B M : ℝ≥0∞}
       (hB : B ≠ ∞) (hM : M ≠ ∞) (hg : ∀ n, Measurable (g n))
       (hρ : ∀ n x, x ∈ O → ρ n x ≤ B) (hgM : ∀ n y, g n y ≤ M)
       (hL : Tendsto (fun n => ∫⁻ y, g n y) atTop (𝓝 0)) :
   …

3. theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_submersion_null_preimage line 105