CutApproximation.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.WeakPinned.Cuts.tent line 39
lemma OAI.WeakPinned.Cuts.tent_nonneg line 40
lemma OAI.WeakPinned.Cuts.tent_symm line 41
lemma OAI.WeakPinned.Cuts.tent_zero_left line 44
lemma OAI.WeakPinned.Cuts.tent_zero_right line 47
lemma OAI.WeakPinned.Cuts.tent_le_one line 50
lemma OAI.WeakPinned.Cuts.tent_lipschitz line 52
lemma OAI.WeakPinned.Cuts.tent_positive line 59
lemma OAI.WeakPinned.Cuts.tent_lower line 63
def OAI.WeakPinned.Cuts.cutError line 66
lemma OAI.WeakPinned.Cuts.cutError_nonneg line 67
lemma OAI.WeakPinned.Cuts.cutError_symm line 69
lemma OAI.WeakPinned.Cuts.cutError_le line 71
lemma OAI.WeakPinned.Cuts.cutError_young line 76
lemma OAI.WeakPinned.Cuts.cutError_tiny line 86
Source documentation
Tiny uniform cells have nonzero balanced-cut weight only if their sampled mass is separated from zero. The variance quadratic then pays the cut error.
```
lemma cutError_tiny {δ p a : ℝ} (hδ : 0<δ) (ha : a<δ/2) (hp : p≤1) :
    cutError δ p a≤(4/δ^2)*(p-a)^2 ∧ cutError δ p a≤(4/δ^2)*(p^2/2) := by
…
```
Mentions: OAI.WeakPinned.Cuts.cutError
def OAI.WeakPinned.Variance.familyCutError line 114
lemma OAI.WeakPinned.Variance.familyCutError_bound line 117
lemma OAI.WeakPinned.Variance.balanced_cell_size line 176
lemma OAI.WeakPinned.Variance.balanced_cell_pair line 186

lemma OAI.WeakPinned.Variance.weighted_cut_approximation line 198

Source documentation

Integrated approximation to balanced tree cuts, quantitatively, with no selection of a realizing grid and no hidden count of occurrence multiplicities.

lemma weighted_cut_approximation (m : Finset P → ℝ) (hm : ∀ C, 0 ≤ m C)
    (w : I → ℝ) (B : I → Finset P) (T δ ε : ℝ)
    (hw : ∀ i, 0≤w i) (hW : (∑ i, w i)≤1) (hδ : 0<δ) (hε : 0<ε)
    (hn : 4≤δ*(Fintype.card P:ℝ)) (hT : T<δ*(Fintype.card P:ℝ)/2)
    (hk : ∀ i, 2/((B i).card:ℝ)≤δ) :
    weightedIntegral m (familyCutError w B δ)≤
      (8*ε/δ^2)*weightedIntegral m (pairCell Finset.univ)+
      (1/ε+4/δ^2)*weightedIntegral m (varianceCell w B T) := by
…

Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Variance.weightedIntegral, OAI.WeakPinned.Variance.familyCutError, OAI.WeakPinned.Variance.pairCell, OAI.WeakPinned.Variance.varianceCell

lemma OAI.WeakPinned.cut_approximation_rate line 230

Source documentation

A Young estimate for every fixed positive ε implies the required little-o cut approximation. D is the actual (positive) overlap normalization.

lemma cut_approximation_rate (E V W D : ℕ → ℝ) (δ K : ℝ) (hδ : 0<δ) (hK : 0<K)
    (hE : ∀ j, 0≤E j) (hD : ∀ j, 0<D j)
    (hW : ∀ᶠ j in atTop, W j≤K*D j)
    (hV : Tendsto (fun j => V j/D j) atTop (𝓝 0))
    (hb : ∀ ε : ℝ, 0<ε → ∀ᶠ j in atTop,
      E j≤(8*ε/δ^2)*W j+(1/ε+4/δ^2)*V j) :
    Tendsto (fun j => E j/D j) atTop (𝓝 0) := by
…

lemma OAI.WeakPinned.variance_to_cut_rate line 271

theorem OAI.WeakPinned.sampling_cut_approximation_rates line 318

Source documentation

Cut approximation for both sampling families, normalized by W₂+A+1 and hence by W in the unbounded regime.

theorem sampling_cut_approximation_rates (δ : ℝ) (hδ : 0<δ) (hθ : 0<θ)
    (hγ : 0<γ) (hγ1 : γ<1) (hc : 0<c) (hcγ : c<γ)
    (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
    (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j, 0≤η j) (hηb : ∀ j, η j≤θ/2)
    (hG : ∀ j, PreparedGraph (V j) (I j) (G j) θ γ c (η j))
    (t : ∀ j, I j → K j) (ht : ∀ j e y, y ∈ (G j).targets e →
      (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e) :
    Tendsto (fun j => weightedIntegral (totalMass (Z₁ j) (Z₂ j) (h₁ j) (h₂ j))
        (familyCutError (G j).fiberWeight (G j).targets δ)/
      (overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+potentialScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+1)) atTop (𝓝 0) ∧
    Tendsto (fun j => weightedIntegral (totalMass (Z₁ j) (Z₂ j) (h₁ j) (h₂ j))
        (familyCutError ((G j).retainedWeight ((Fintype.card (V j):ℝ)^γ))
…

Mentions: OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale