MultipointUniformCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A single finite-order Young coefficient controls every active subset. The coefficient is chosen before the stopping-time pattern is known.

def OAI.SLEExactGauge.Multipoint.patternYoungConstant line 14
Source documentation
The Young coefficient associated with one active subset.
```
def patternYoungConstant {ι : Type*} (κ : ℝ) (s : Finset ι) : ℝ :=
…
```
def OAI.SLEExactGauge.Multipoint.allPatternYoungConstant line 20
Source documentation
A common coefficient for all active subsets of a fixed finite family.
```
def allPatternYoungConstant {ι : Type*} (κ : ℝ) (I : Finset ι) : ℝ :=
…
```
lemma OAI.SLEExactGauge.Multipoint.patternYoungConstant_pos line 23
lemma OAI.SLEExactGauge.Multipoint.patternYoungConstant_le_all line 33
lemma OAI.SLEExactGauge.Multipoint.allPatternYoungConstant_pos line 39

theorem OAI.SLEExactGauge.Multipoint.productDriftCost_le_uniform line 47

Source documentation

The actual drift cost is controlled by one deterministic coefficient, while keeping precisely the current active single and pair sums.

theorem productDriftCost_le_uniform {ι : Type*} [DecidableEq ι]
    {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8) {I s : Finset ι} (hs : s ⊆ I)
    (D σ : ι → ℝ) (hD : ∀ i ∈ s, 0 < D i) (z : ι → ℂ × ℝ) (x : ℝ) :
    productDriftCost s κ D σ z x ≤
      κ*((driftAllowance (greenExponent κ)*
          driftThreshold (greenExponent κ)^(-greenExponent κ))*
        (∑ i ∈ s, branchRegulator κ (D i) (σ i) (z i)*logVelocity κ (z i) x^2) +
        allPatternYoungConstant κ I *
          (∑ ij ∈ s.offDiag,
            (branchRegulator κ (D ij.1) (σ ij.1) (z ij.1)*
              branchRegulator κ (D ij.2) (σ ij.2) (z ij.2))^(-exponent (greenExponent κ))*
            (logVelocity κ (z ij.1) x*logVelocity κ (z ij.2) x))) := by
…

Mentions: OAI.SLEExactGauge.Multipoint.productDriftCost, OAI.SLEExactGauge.Multipoint.driftAllowance, OAI.SLEExactGauge.greenExponent, OAI.SLEExactGauge.Multipoint.driftThreshold, OAI.SLEExactGauge.Multipoint.branchRegulator, OAI.SLEExactGauge.Multipoint.logVelocity, OAI.SLEExactGauge.Multipoint.allPatternYoungConstant, OAI.SLEExactGauge.Multipoint.exponent