OAI/Analysis/CircleDomains/Probability/HitFusion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fusion of a nonsmall closed family of path laws into a law with finite point-hit square norm. All finite splitting and branch laws are constructed.

  1. def OAI.CircleDomainRigidity.HitFusionData.fusedLaw line 27
  2. theorem OAI.CircleDomainRigidity.HitFusionData.weighted_fusedLaw line 32
  3. theorem OAI.CircleDomainRigidity.HitFusionData.fusedLaw_configuration_bound line 47
  4. def OAI.CircleDomainRigidity.standardHitFusion line 56
  5. theorem OAI.CircleDomainRigidity.standardHitFusion_norm_bound line 66
  6. theorem OAI.CircleDomainRigidity.exists_hit_norm_mixture_of_nonsmall line 85

    Source documentation

    The fused law is supported on original candidates, not merely limits of arbitrary probability laws. Its positive point-hit support is countable.

    theorem exists_hit_norm_mixture_of_nonsmall (hlaw : Continuous law) (hC : 0 ≤ C)
    {A : Set Z} (hAclosed : IsClosed A) (hA : ¬HitTestSmall law C A)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (P : ProbabilityMeasure (ℕ → ℕ)) (e : C(ℕ → ℕ, Z)),
      (∀ x, e x ∈ A) ∧
      HasHitNormBound (probabilityMixture P (law ∘ e) (measurable_of_continuous_probability (hlaw.comp e.continuous)))
        (C + ε) := by
…

    Mentions: OAI.CircleDomainRigidity.HitTestSmall, OAI.CircleDomainRigidity.HasHitNormBound, OAI.CircleDomainRigidity.probabilityMixture, OAI.CircleDomainRigidity.measurable_of_continuous_probability

  7. theorem OAI.CircleDomainRigidity.exists_hit_norm_mixture_of_countable_tests line 101

    Source documentation

    The original countable and atomless tests supply the nonsmall root of the constructed fusion tree.

    theorem exists_hit_norm_mixture_of_countable_tests
    (hlaw : Continuous law) (hC : 0 ≤ C)
    (htest : ∀ D : Set X, D.Countable → ∀ ν : Measure X,
      IsFiniteMeasure ν → NullSingletonClass ν → ∃ z, PassesHitTests C (law z) D ν)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (P : ProbabilityMeasure (ℕ → ℕ)) (e : C(ℕ → ℕ, Z)),
      HasHitNormBound (probabilityMixture P (law ∘ e)
        (measurable_of_continuous_probability (hlaw.comp e.continuous))) (C + ε) := by
…

    Mentions: OAI.CircleDomainRigidity.PassesHitTests, OAI.CircleDomainRigidity.HasHitNormBound, OAI.CircleDomainRigidity.probabilityMixture, OAI.CircleDomainRigidity.measurable_of_continuous_probability