OAI/MathematicalPhysics/Boltzmann/Jets/GeometricMesh.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

A compact logarithmic phase for the dilated geometric mesh

  1. def OAI.BoltzmannNonuniqueness.GeometricMesh.phase line 21
  2. def OAI.BoltzmannNonuniqueness.GeometricMesh.index line 23
  3. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.phase_bounds line 25
  4. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.normalization line 32
  5. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.scale_ratio line 42
  6. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.phase_subsequence line 54
  7. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.index_tendsto_atTop line 76
  8. def OAI.BoltzmannNonuniqueness.GeometricMesh.annularIndex line 87
  9. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.annularIndex_eventually line 90
  10. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.mesh_point_approximation line 102
  11. def OAI.BoltzmannNonuniqueness.GeometricMesh.point line 128
  12. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_pos line 130
  13. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_mono line 133
  14. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_succ line 140
  15. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_gap line 145
  16. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.shells_disjoint line 150
  17. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.phase_lt_exp line 159
  18. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.cell_bounds line 163
  19. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.eventually_retained line 199
  20. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.eventually_below_terminal line 212
  21. def OAI.BoltzmannNonuniqueness.GeometricBackground.scale line 243
  22. def OAI.BoltzmannNonuniqueness.GeometricBackground.active line 248

    Source documentation

    Here l is the limit of the first excluded scale scale (N+1) / r. The retained colors have strictly larger scales.

    def active (θ η l : ℝ) (y : Transverse) : Prop :=
…
  23. def OAI.BoltzmannNonuniqueness.GeometricBackground.background line 251
  24. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scale_pos line 255
  25. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scale_measurable line 258
  26. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.active_measurableSet line 262
  27. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scale_eq_of_shell line 267
  28. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_on_shell line 279
  29. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_gain_bound line 288
  30. def OAI.BoltzmannNonuniqueness.GeometricMesh.jetIndex line 326
  31. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.annularIndex_eventually_pos line 329
  32. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jetIndex_succ_eventually line 337
  33. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jet_scale_approximation line 344
  34. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jetIndex_eventually_retained line 354
  35. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_strictMono line 381
  36. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.shell_index line 388
  37. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.index_mono line 394
  38. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.shell_index_window line 398
  39. def OAI.BoltzmannNonuniqueness.GeometricMesh.jetMeshIndex line 415

    Source documentation

    The integer mesh coordinate of an actual jet label.

    def jetMeshIndex (s₀ η r : ℝ) (j : ℕ) : ℤ := index (s₀/r) η-(j+1:ℕ)

    Mentions: OAI.BoltzmannNonuniqueness.GeometricMesh.index

  40. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jetScale_ratio_exact line 417
  41. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jetIndex_at_meshIndex line 424
  42. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.meshIndex_at_jetIndex line 442
  43. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.finite_sum_on_window line 449
  44. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.index_point_div_phase line 487
  45. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.point_window line 493
  46. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.jetMeshIndex_injective line 510
  47. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.retained_scale_card_le line 516

    Source documentation

    The bound is independent of the dilation and of the retained top index.

    theorem retained_scale_card_le {s₀ η r δ R : ℝ} (hs₀ : 0 < s₀) (hη : 0 < η)
    (hr : 0 < r) (hδ : 0 < δ) (J : Finset ℕ)
    (hJ : ∀ j ∈ J, δ ≤ JetGeometry.jetScale s₀ η j/r ∧
      JetGeometry.jetScale s₀ η j/r ≤ R) :
    J.card ≤ (Finset.Icc (index (δ/Real.exp η) η) (index R η)).card := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetGeometry.jetScale, OAI.BoltzmannNonuniqueness.GeometricMesh.index

  48. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.scale_succ line 548
  49. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.scale_gap line 556
  50. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.indices_eventually_eq_of_same_positive_limit line 563
  51. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.mesh_scale_tendsto_zero line 601
  52. theorem OAI.BoltzmannNonuniqueness.GeometricMesh.mesh_width_tendsto_zero line 612