OAI/Geometry/PinnedDistances/MobiusObstruction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.Bounded.crossKernel line 14
  2. def OAI.WeakPinned.Bounded.targetKernel line 17
  3. def OAI.WeakPinned.Bounded.crossEnergy line 20
  4. def OAI.WeakPinned.Bounded.targetEnergy line 23
  5. lemma OAI.WeakPinned.Bounded.measurable_crossKernel line 26
  6. lemma OAI.WeakPinned.Bounded.measurable_targetKernel line 30
  7. lemma OAI.WeakPinned.Bounded.crossKernel_nonneg line 34
  8. lemma OAI.WeakPinned.Bounded.crossKernel_le_one line 37
  9. lemma OAI.WeakPinned.Bounded.targetKernel_nonneg line 40
  10. lemma OAI.WeakPinned.Bounded.targetKernel_le_one line 43
  11. lemma OAI.WeakPinned.Bounded.integrable_crossKernel line 46
  12. lemma OAI.WeakPinned.Bounded.integrable_targetKernel line 54
  13. lemma OAI.WeakPinned.Bounded.crossKernel_tendsto line 62
  14. lemma OAI.WeakPinned.Bounded.ae_pair_ne line 72
  15. lemma OAI.WeakPinned.Bounded.crossEnergy_tendsto line 81
  16. lemma OAI.WeakPinned.Bounded.ae_distinct_pair line 94
  17. lemma OAI.WeakPinned.Bounded.targetEnergy_pos line 101
  18. lemma OAI.WeakPinned.Bounded.not_ae_energy_eq line 117
  19. lemma OAI.WeakPinned.Bounded.measurable_crossEnergy line 132
  20. lemma OAI.WeakPinned.Bounded.measurable_targetEnergy line 140
  21. def OAI.WeakPinned.Bounded.mobius line 147
  22. lemma OAI.WeakPinned.Bounded.measurable_mobius line 149
  23. lemma OAI.WeakPinned.Bounded.mobius_sub_target line 153
  24. lemma OAI.WeakPinned.Bounded.mobius_ne_target line 159
  25. lemma OAI.WeakPinned.Bounded.kernel_mobius line 166
  26. lemma OAI.WeakPinned.Bounded.energy_of_mobius_map line 181
  27. lemma OAI.WeakPinned.Bounded.measurableSet_energy_eq line 197
  28. theorem OAI.WeakPinned.Bounded.no_finite_law line 210

    Source documentation

    The finite-plane non-atomic obstruction.

    theorem no_finite_law (μ ν : Measure ℂ) [IsProbabilityMeasure μ]
    [IsProbabilityMeasure ν] [NullSingletonClass μ] [NullSingletonClass ν]
    (Q : Measure (ℂ × ℂ × ℂ × ℂ)) [IsProbabilityMeasure Q]
    (hlaw : Q.map (fun q => q.1) = μ)
    (hind : ProbabilityTheory.IndepFun (fun q => q.1) (fun q => q.2.2) Q)
    (hsupp : ∀ᵐ q ∂ Q, q.2.2.1 ∈ μ.support)
    (hbd : ∀ᵐ q ∂ Q, q.2.1 ≠ q.2.2.2)
    (hmap : ∀ᵐ q ∂ Q, μ.map (mobius q.1 q.2.1 q.2.2.1 q.2.2.2) = ν) : False := by
…

    Mentions: OAI.WeakPinned.Bounded.mobius

  29. abbrev OAI.WeakPinned.Bounded.Sphere line 241

    Source documentation

    The Riemann sphere as the one-point compactification of the complex plane.

    abbrev Sphere := OnePoint ℂ
…
  30. lemma OAI.WeakPinned.Bounded.measurableEmbedding_sphere_coe line 245
  31. def OAI.WeakPinned.Bounded.sphereMobius line 250

    Source documentation

    The sphere Möbius map has its pole at infinity and its value at infinity is b; no finite-valued division convention is used there.

    def sphereMobius (a b c d : ℂ) : Sphere → Sphere :=
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  32. lemma OAI.WeakPinned.Bounded.sphereMobius_coe line 254
  33. lemma OAI.WeakPinned.Bounded.sphereMobius_pole line 258
  34. lemma OAI.WeakPinned.Bounded.sphereMobius_infty line 262
  35. lemma OAI.WeakPinned.Bounded.map_sphereMobius line 265
  36. lemma OAI.WeakPinned.Bounded.finite_map_of_sphere_map line 281
  37. theorem OAI.WeakPinned.Bounded.bounded_mobius line 290

    Source documentation

    The non-atomic Möbius obstruction with its pushforward identity on the Riemann sphere.

    theorem bounded_mobius (μ ν : Measure ℂ) [IsProbabilityMeasure μ]
    [IsProbabilityMeasure ν] [NullSingletonClass μ] [NullSingletonClass ν]
    (Q : Measure (ℂ × ℂ × ℂ × ℂ)) [IsProbabilityMeasure Q]
    (hsep : ∀ᵐ q ∂ Q, q.1 ≠ q.2.2.1 ∧ q.2.1 ≠ q.2.2.2)
    (hsupp : ∀ᵐ q ∂ Q, q.2.2.1 ∈ μ.support ∧ q.2.2.2 ∈ ν.support)
    (hlaw : Q.map (fun q => q.1) = μ)
    (hind : ProbabilityTheory.IndepFun (fun q => q.1) (fun q => q.2.2) Q)
    (hmap : ∀ᵐ q ∂ Q, (μ.map ((↑) : ℂ → Sphere)).map
      (sphereMobius q.1 q.2.1 q.2.2.1 q.2.2.2) = ν.map ((↑) : ℂ → Sphere)) : False := by
…

    Mentions: OAI.WeakPinned.Bounded.Sphere, OAI.WeakPinned.Bounded.sphereMobius

  38. instance OAI.WeakPinned.Bounded.sphereSecondCountable line 311

    Source documentation

    The one-point compactification of the complex plane has a countable basis.

    instance sphereSecondCountable : SecondCountableTopology Sphere := by
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  39. lemma OAI.WeakPinned.Bounded.sphere_pair_subsequence line 346
  40. lemma OAI.WeakPinned.Bounded.weak_open_bound line 354

    Source documentation

    A useful Portmanteau consequence with an eventual bound; measures, not arbitrary test function samples, are passed to the limit.

    lemma weak_open_bound {α : ℕ → ProbabilityMeasure Sphere} {β : ProbabilityMeasure Sphere}
    (hT : Tendsto α atTop (𝓝 β)) {U : Set Sphere} (hU : IsOpen U) (b : ℝ≥0∞)
    (hbound : ∀ᶠ n in atTop, (α n : Measure Sphere) U ≤ b) :
    (β : Measure Sphere) U ≤ b := by
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  41. lemma OAI.WeakPinned.Bounded.weak_singleton_zero line 362

    Source documentation

    Neighborhood control is enough to remove a possible atom in a weak limit.

    lemma weak_singleton_zero {α : ℕ → ProbabilityMeasure Sphere} {β : ProbabilityMeasure Sphere}
    (hT : Tendsto α atTop (𝓝 β)) (z : Sphere)
    (hsmall : ∀ ε : ℝ, 0 < ε → ∃ U : Set Sphere, IsOpen U ∧ z ∈ U ∧
      ∀ᶠ n in atTop, (α n : Measure Sphere) U ≤ ENNReal.ofReal ε) :
    (β : Measure Sphere) {z}=0 := by
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  42. theorem OAI.WeakPinned.Bounded.weak_limit_nonatomic line 378

    Source documentation

    Finiteness and nonatomicity on the sphere follow from open-tail and disk bounds through the Portmanteau inequality.

    theorem weak_limit_nonatomic {α : ℕ → ProbabilityMeasure Sphere} {β : ProbabilityMeasure Sphere}
    (hT : Tendsto α atTop (𝓝 β))
    (htail : ∀ ε : ℝ, 0 < ε → ∃ R : ℝ, ∀ᶠ n in atTop,
      (α n : Measure Sphere) (OnePoint.some '' Metric.closedBall (0:ℂ) R)ᶜ ≤ ENNReal.ofReal ε)
    (hball : ∀ z : ℂ, ∀ ε : ℝ, 0 < ε → ∃ r : ℝ, 0 < r ∧ ∀ᶠ n in atTop,
      (α n : Measure Sphere) (OnePoint.some '' Metric.ball z r) ≤ ENNReal.ofReal ε) :
    NullSingletonClass (β : Measure Sphere) := by
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  43. def OAI.WeakPinned.Bounded.finitePart line 400

    Source documentation

    Restriction of a sphere probability measure to the complex plane. This is a probability measure when there is no mass at infinity.

    def finitePart (β : ProbabilityMeasure Sphere) : Measure ℂ :=
…

    Mentions: OAI.WeakPinned.Bounded.Sphere

  44. lemma OAI.WeakPinned.Bounded.finitePart_probability line 403
  45. lemma OAI.WeakPinned.Bounded.finitePart_nonatomic line 411
  46. lemma OAI.WeakPinned.Bounded.finitePart_map line 417