MarkedHitFusion.lean`

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.

def OAI.CircleDomainRigidity.MarkedHit.HitFusionData.fusedLaw line 30
theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.weighted_fusedLaw line 36
theorem OAI.CircleDomainRigidity.MarkedHit.HitFusionData.fusedLaw_configuration_bound line 52
def OAI.CircleDomainRigidity.MarkedHit.standardHitFusion line 61
theorem OAI.CircleDomainRigidity.MarkedHit.standardHitFusion_norm_bound line 71
theorem OAI.CircleDomainRigidity.MarkedHit.exists_hit_norm_mixture_of_nonsmall line 90
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.MarkedHit.HitTestSmall, OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound, OAI.CircleDomainRigidity.probabilityMixture, OAI.CircleDomainRigidity.measurable_of_continuous_probability

theorem OAI.CircleDomainRigidity.MarkedHit.exists_hit_norm_mixture_of_countable_tests line 106

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.MarkedHit.PassesHitTests, OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound, OAI.CircleDomainRigidity.probabilityMixture, OAI.CircleDomainRigidity.measurable_of_continuous_probability