OAI/MathematicalPhysics/Boltzmann/Branching/FiveGainPullback.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Rank seven of the actual map at the explicit collision witness

  1. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rank_at_witness line 25
  2. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.rank_rotation line 99
  3. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.exists_nonaxial_rank_point line 125
  4. theorem OAI.BoltzmannNonuniqueness.PositiveIteration.five_tendsto_of_time_cutoffs line 171
  5. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.map_rank_ae line 232
  6. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.controlDerivative_zero_apply line 259
  7. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.controlDerivative_zero_surjective line 279
  8. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.zeroWidth_rank_ae line 306
  9. def OAI.BoltzmannNonuniqueness.FiveGainMap.controlDomain line 342
  10. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.controlDomain_open line 344
  11. def OAI.BoltzmannNonuniqueness.FiveGainMap.controlCoordinates line 348

    Source documentation

    Seven output coordinates and twenty-eight complementary parameters.

    def controlCoordinates : ThermalControls ≃L[ℝ] State × (Fin 28 → ℝ) :=
…

    Mentions: OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalControls, OAI.BoltzmannNonuniqueness.FiveGainMap.State

  12. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.controlDerivative_continuousAt line 353
  13. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermal_compact_pullback_zero line 365

    Source documentation

    Uniformly bounded parameter densities pull local L1 errors back to zero through the five thermal gains, at any nonaxial limiting endpoint.

    theorem thermal_compact_pullback_zero (hMityagin : Published.Mityagin2020FiveGainParameters)
    {σ μ : Fin 5 → ℝ} {α γ : ℝ} (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hμ : ∀ i, 0 < μ i) (t₀ : ℝ) (x v : V) (hv : 0 < v 0^2+v 1^2)
    {env : ℕ → PositiveEnvironment}
    (henv : Tendsto env atTop (𝓝 (⟨(μ,0,(t₀,x,v)),hμ⟩ : PositiveEnvironment)))
    {K : Set ThermalControls} (hK : IsCompact K) (hKT : K ⊆ controlDomain)
    {g : ℕ → State → ℝ≥0∞} {ρ : ℕ → ThermalControls → ℝ≥0∞} {B M : ℝ≥0∞}
    (hB : B ≠ ∞) (hM : M ≠ ∞) (hg : ∀ n, Measurable (g n))
    (hρ : ∀ n q, q ∈ controlDomain → ρ n q ≤ B) (hgM : ∀ n z, g n z ≤ M)
    (hL : Tendsto (fun n => ∫⁻ z, g n z) atTop (𝓝 0)) :
    Tendsto (fun n => ∫⁻ q in K, ρ n q*g n (thermalMap σ α γ ((env n).val,q)))
      atTop (𝓝 0) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.Mityagin2020FiveGainParameters, OAI.BoltzmannNonuniqueness.FiveGainMap.V, OAI.BoltzmannNonuniqueness.FiveGainMap.PositiveEnvironment, OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalControls, OAI.BoltzmannNonuniqueness.FiveGainMap.controlDomain, OAI.BoltzmannNonuniqueness.FiveGainMap.State, OAI.BoltzmannNonuniqueness.FiveGainMap.thermalMap

  14. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermal_compact_pullback_zero_local line 423

    Source documentation

    Only the values on one fixed output ball enter a compact parameter integral.

    theorem thermal_compact_pullback_zero_local
    (hMityagin : Published.Mityagin2020FiveGainParameters)
    {σ μ : Fin 5 → ℝ} {α γ : ℝ} (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hμ : ∀ i, 0 < μ i) (t₀ : ℝ) (x v : V) (hv : 0 < v 0^2+v 1^2)
    {env : ℕ → PositiveEnvironment}
    (henv : Tendsto env atTop (𝓝 (⟨(μ,0,(t₀,x,v)),hμ⟩ : PositiveEnvironment)))
    {K : Set ThermalControls} (hK : IsCompact K) (hKT : K ⊆ controlDomain)
    {g : ℕ → State → ℝ≥0∞} {ρ : ℕ → ThermalControls → ℝ≥0∞} {B M : ℝ≥0∞}
    (hB : B ≠ ∞) (hM : M ≠ ∞) (hg : ∀ n, Measurable (g n))
    (hρ : ∀ n q, q ∈ controlDomain → ρ n q ≤ B) (hgM : ∀ n z, g n z ≤ M)
    (hL : ∀ R : ℝ, 0 < R → Tendsto
      (fun n => ∫⁻ z in closedBall (0 : State) R, g n z) atTop (𝓝 0)) :
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.Mityagin2020FiveGainParameters, OAI.BoltzmannNonuniqueness.FiveGainMap.V, OAI.BoltzmannNonuniqueness.FiveGainMap.PositiveEnvironment, OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalControls, OAI.BoltzmannNonuniqueness.FiveGainMap.controlDomain, OAI.BoltzmannNonuniqueness.FiveGainMap.State

  15. def OAI.BoltzmannNonuniqueness.FiveGainMap.toKinetic line 494
  16. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.toKinetic_apply line 499
  17. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.toKinetic_measurePreserving line 502
  18. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.toKinetic_continuous line 526
  19. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermal_compact_pullback_zero_physical line 533
  20. def OAI.BoltzmannNonuniqueness.FiveGainMap.stagePrevious line 584
  21. def OAI.BoltzmannNonuniqueness.FiveGainMap.stagePosition line 588
  22. def OAI.BoltzmannNonuniqueness.FiveGainMap.stagePoint line 593
  23. def OAI.BoltzmannNonuniqueness.FiveGainMap.stageDensity line 599
  24. def OAI.BoltzmannNonuniqueness.FiveGainMap.pathDensity line 605
  25. def OAI.BoltzmannNonuniqueness.FiveGainMap.stageGood line 609
  26. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.stageDensity_bound line 614
  27. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.masked_pathDensity_bound line 624
  28. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.five_gain_parameter_tendsto line 645
  29. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_continuous_positive line 695
  30. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.stageDensity_measurable_positive line 707
  31. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.pathDensity_measurable_positive line 736
  32. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.masked_path_integrand_measurable line 744
  33. abbrev OAI.BoltzmannNonuniqueness.FiveGainMap.StageControls line 787
  34. def OAI.BoltzmannNonuniqueness.FiveGainMap.packControls line 789
  35. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.packControls_apply line 794
  36. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.packControls_measurePreserving line 797
  37. def OAI.BoltzmannNonuniqueness.FiveGainMap.integrateControls line 802
  38. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.integrateControls_eq line 806
  39. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.five_gain_product_integral line 831
  40. def OAI.BoltzmannNonuniqueness.FiveGainMap.velocityParameterBall line 854
  41. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.mem_velocityParameterBall line 857
  42. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.velocityParameterBall_compact line 866
  43. def OAI.BoltzmannNonuniqueness.FiveGainMap.parameterBox line 869
  44. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.parameterBox_compact line 874
  45. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.mem_parameterBox line 879
  46. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.parameterBox_subset_domain line 891