PullbackRegularLimit.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Quantitative chart estimates for the finite-gain pullback

A normalized derivative within one half of the identity gives an injective chart. A positive Jacobian lower bound then controls pullback integrals, including arbitrary bounded measurable masks in the parameter density.

theorem OAI.BoltzmannNonuniqueness.GainPullback.chart_injective line 34
theorem OAI.BoltzmannNonuniqueness.GainPullback.jacobian_pullback_bound line 50
theorem OAI.BoltzmannNonuniqueness.GainPullback.masked_jacobian_pullback_bound line 69
theorem OAI.BoltzmannNonuniqueness.GainPullback.regular_derivative_neighborhood line 106

theorem OAI.BoltzmannNonuniqueness.GainPullback.eventually_regular_ball line 130

Source documentation

On a small ball at a regular point, all sufficiently late charts are injective with one common positive Jacobian lower bound.

theorem eventually_regular_ball {O : Set E} (hO : IsOpen O) {x₀ : E} (hx₀ : x₀ ∈ O)
    {f' : E → E →L[ℝ] E} (hcont : ContinuousAt f' x₀)
    (A : E ≃L[ℝ] E) (hAt : f' x₀ = A.toContinuousLinearMap)
    (hA : 0 < |A.toContinuousLinearMap.det|)
    {F : ℕ → E → E} {F' : ℕ → E → E →L[ℝ] E}
    (hF : ∀ n, ∀ x ∈ O, HasFDerivAt (F n) (F' n x) x)
    (hconv : ∀ r > 0, ball x₀ r ⊆ O →
      TendstoUniformlyOn F' f' atTop (ball x₀ r)) :
    ∃ r > 0, ball x₀ r ⊆ O ∧
      ∀ᶠ n in atTop, InjOn (F n) (ball x₀ r) ∧
        ∀ x ∈ ball x₀ r, |A.toContinuousLinearMap.det|/2 ≤ |(F' n x).det| := by
…

theorem OAI.BoltzmannNonuniqueness.GainPullback.tendsto_masked_chart_zero line 184
theorem OAI.BoltzmannNonuniqueness.GainPullback.masked_exception_bound line 204
theorem OAI.BoltzmannNonuniqueness.GainPullback.lintegral_finite_union_le line 232

theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_integral_zero_of_local line 245

Source documentation

Local integral convergence on a neighborhood of each noncritical point suffices on a compact set, provided the integrands have a common bound.

theorem compact_integral_zero_of_local {X : Type*} [TopologicalSpace X]
    [MeasurableSpace X] [BorelSpace X] [T2Space X]
    {μ : Measure X} [OuterRegular μ] {K Z : Set X} (hK : IsCompact K)
    (hZ : μ Z = 0) {f : ℕ → X → ℝ≥0∞} {M : ℝ≥0∞} (hM : M ≠ ∞)
    (hbound : ∀ n x, x ∈ K → f n x ≤ M)
    (hlocal : ∀ x ∈ K \ Z, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧
      Tendsto (fun n => ∫⁻ y in U, f n y ∂μ) atTop (𝓝 0)) :
    Tendsto (fun n => ∫⁻ x in K, f n x ∂μ) atTop (𝓝 0) := by
…

theorem OAI.BoltzmannNonuniqueness.GainPullback.product_chart_bound line 319
theorem OAI.BoltzmannNonuniqueness.GainPullback.tendsto_product_chart_zero line 347
theorem OAI.BoltzmannNonuniqueness.GainPullback.augmented_derivative_uniform line 392
theorem OAI.BoltzmannNonuniqueness.GainPullback.local_augmented_pullback_zero line 414
theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_submersion_pullback_zero line 482

theorem OAI.BoltzmannNonuniqueness.GainPullback.compact_regular_pullback_zero line 528

Source documentation

The square-map case of the robust pullback estimate. Neither the masks nor the bounded integrands are required to converge pointwise.

theorem compact_regular_pullback_zero {O K Z : Set E} (hO : IsOpen O)
    (hK : IsCompact K) (hKO : K ⊆ O) (hZ : μ Z = 0)
    {F : ℕ → E → E} {F' : ℕ → E → E →L[ℝ] E} {f' : E → E →L[ℝ] E}
    (hder : ∀ n, ∀ x ∈ O, HasFDerivAt (F n) (F' n x) x)
    (hcont : ∀ x ∈ O, ContinuousAt f' x)
    (hreg : ∀ x ∈ K \ Z, ∃ A : E ≃L[ℝ] E, f' x = A.toContinuousLinearMap)
    (hconv : ∀ x ∈ O, ∀ r > 0, ball x r ⊆ O →
      TendstoUniformlyOn F' f' atTop (ball x r))
    {g ρ : ℕ → E → ℝ≥0∞} {B M : ℝ≥0∞} (hB : B ≠ ∞) (hM : M ≠ ∞)
    (hρ : ∀ n x, x ∈ O → ρ n x ≤ B) (hg : ∀ n y, g n y ≤ M)
    (hL : Tendsto (fun n => ∫⁻ y, g n y ∂μ) atTop (𝓝 0)) :
    Tendsto (fun n => ∫⁻ x in K, ρ n x*g n (F n x) ∂μ) atTop (𝓝 0) := by
…