OAI/MathematicalPhysics/Boltzmann/Branching/PullbackCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_pullback_zero_coordinates line 26

   Source documentation

   The domain coordinates may differ from the output plus complementary coordinates. Only compact-local convergence of the derivatives is needed.

   theorem compact_pullback_zero_coordinates (e : E ≃L[ℝ] P × Q)
       {μ : Measure E} [IsAddHaarMeasure μ]
       {O K Z : Set E} (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O) (hZ : μ 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 : ∀ C : Set E, IsCompact C → C ⊆ O → TendstoUniformlyOn Φ' φ' atTop C)
       {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)) :
   …