CanonicalGridLower.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite centered-law tests which suffice for the prescribed lower bound. The half-threshold and the factor two come from actual past-mass detection.

lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.compact_spatial_bad_charge_of_finite_tests line 28

theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.ae_positive_prescribed_of_finite_tests line 51

Source documentation

Finite centered-law bounds imply the prescribed lower-bound criterion. The gauge and its positive moments are the prescribed nested Wiener coefficients.

theorem ae_positive_prescribed_of_finite_tests [IsProbabilityMeasure P]
    (hpublished : PublishedTraceGeneration (P.map (sourceDriverPath B hc)) κ (fun t p => p t))
    (hgrowth : PublishedDiskUnivalentGrowth) (W : Target.WienerLaw) (hW : Target.IsWiener W)
    (u : ℕ → ℝ) (hu : ∀ n, 0 ≤ u n) (hmono : Monotone u)
    (hlim : Tendsto u atTop atTop) (q : ℕ → ℝ≥0) (hq : DenseRange q)
    (K : Set upperHalfPlane) (hK : IsCompact K) (D : ℝ) (hD : 0 < D)
    (p : Target.GaugeIndex κ W → ℝ≥0∞) (hp : (∑' e, p e) ≠ ∞)
    (hbound : ∀ e : Target.GaugeIndex κ W, ∀ i : ℤ×ℤ, ∀ j, ∀ᶠ n in atTop,
      (∫⁻ x in (Subtype.val : upperHalfPlane → ℂ) ''
          (K ∩ Subtype.val ⁻¹' closedBall (coverGridCenter (Target.radii κ W e) i)
            (2*Target.radii κ W e)),
        ENNReal.ofReal (initialGreen κ x) * finiteCenteredLaw P κ B γ G x (u n)
…

Mentions: OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth, OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.IsWiener, OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.Target.GaugeIndex, OAI.SLEExactGauge.coverGridCenter, OAI.SLEExactGauge.Target.radii, OAI.SLEExactGauge.initialGreen, OAI.SLEExactGauge.finiteCenteredLaw