UniformCore.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

def OAI.WeakPinned.Core.Fibers.retained line 36
Source documentation
Retain a specified family of the original fibers, restricted to D. This never alters a source or creates a new distance coincidence.
```
def retained (D : Finset V) (Q : I → Prop) [DecidablePred Q] : Fibers V I where
…
```
Mentions: OAI.WeakPinned.Core.Fibers
lemma OAI.WeakPinned.Core.Fibers.retained_card line 52
def OAI.WeakPinned.heavyFiber line 72
instance OAI.WeakPinned.(instance at line 77) line 77
lemma OAI.WeakPinned.heavySubset_edge_rich line 80
theorem OAI.WeakPinned.heavySubset_count line 111
Source documentation
The exact finite counting step underlying both uniform subset estimates for the rich-pair graph. Each ordered pair is counted only once.
```
theorem heavySubset_count (P : Finset Plane) (s K lam r : ℝ) (C D : Finset P)
    (hlam : 0 ≤ lam) (hK : (D.card : ℝ)^r ≤ lam*K) :
    (∑ e, if heavyFiber P s K lam C D e ∧ (planarFibers P s).source e ∈ D
      then ((planarFibers P s).size D e : ℝ) else 0) ≤
      (richPairs (planeSubset P D) r).card := by
…
```
Mentions: OAI.WeakPinned.Plane, OAI.WeakPinned.heavyFiber, OAI.WeakPinned.planarFibers, OAI.WeakPinned.richPairs, OAI.WeakPinned.planeSubset
def OAI.WeakPinned.Theta line 131
lemma OAI.WeakPinned.F_bdd line 133
lemma OAI.WeakPinned.F_cobdd line 135
lemma OAI.WeakPinned.Theta_nonneg line 138
lemma OAI.WeakPinned.Theta_le_one line 144
lemma OAI.WeakPinned.Theta_antitone line 147
lemma OAI.WeakPinned.Theta_eq_zero_of_one_le line 151
lemma OAI.WeakPinned.tendsto_F_of_Theta_zero line 154
def OAI.WeakPinned.criticalExponent line 162
lemma OAI.WeakPinned.positive_exponents_bdd line 164
lemma OAI.WeakPinned.failed_main_nonempty line 171
lemma OAI.WeakPinned.critical_pos line 179
lemma OAI.WeakPinned.critical_le_one line 183
lemma OAI.WeakPinned.Theta_pos_below_critical line 189
lemma OAI.WeakPinned.Theta_zero_above_critical line 193

theorem OAI.WeakPinned.extremal_parameters line 203

Source documentation

A fixed exponent regime obtained from failure of the uniform multiplicity limit.

theorem extremal_parameters (h : ¬ MainStatement) :
    ∃ c s γ : ℝ, 0 < c ∧ c < criticalExponent/3 ∧
      max c ((1-c)*criticalExponent) < s ∧ s < criticalExponent ∧
      c < γ ∧ γ < s ∧ ContinuousAt Theta s ∧ 0 < Theta s := by
…

Mentions: OAI.WeakPinned.MainStatement, OAI.WeakPinned.criticalExponent, OAI.WeakPinned.Theta

lemma OAI.WeakPinned.extremal_subsequence line 223

lemma OAI.WeakPinned.extremal_tail line 230

Source documentation

The epsilon-uniform extremal tail bound. The lower cutoff may vary arbitrarily provided it tends to infinity.

lemma extremal_tail {s : ℝ} (hs : ContinuousAt Theta s) {r : ℕ → ℝ} {M : ℕ → ℕ}
    (hr : Tendsto r atTop (𝓝 s)) (hM : Tendsto M atTop atTop) :
    ∀ ε > 0, ∀ᶠ i in atTop, ∀ m : ℕ, M i ≤ m → F m (r i) ≤ Theta s+ε := by
…

Mentions: OAI.WeakPinned.Theta, OAI.WeakPinned.F

def OAI.WeakPinned.cutoff line 257
lemma OAI.WeakPinned.eventual_power_below_cutoff line 259
lemma OAI.WeakPinned.eventual_cutoff_loss line 274
lemma OAI.WeakPinned.continuous_left_tail line 295
lemma OAI.WeakPinned.half_boundary line 311

theorem OAI.WeakPinned.arbitrarily_large_core line 327

Source documentation

Actual core configurations at arbitrarily small density error and arbitrarily large cardinality. No field or position assumptions are introduced.

theorem arbitrarily_large_core {s γ : ℝ} (hγ : 0 < γ) (hγs : γ < s)
    (hs : ContinuousAt Theta s) (η : ℝ) (hη : 0 < η) (M : ℕ) :
    ∃ (P : Finset Plane) (C : Finset P), M < C.card ∧
      (P.card+1)/2 < C.card ∧ (C.card : ℝ)^γ ≤ cutoff s P.card ∧
      (Theta s-η)*(C.card : ℝ)*((C.card : ℝ)-1) ≤ ((planarFibers P s).edgeSet (cutoff s P.card) C).card ∧
      (((planarFibers P s).edgeSet (cutoff s P.card) C).card : ℝ) ≤
        (Theta s+η/8)*(C.card : ℝ)*((C.card : ℝ)-1) ∧
      (∀ x ∈ C, 2*(Theta s-η)*((C.card : ℝ)-1) ≤
        (planarFibers P s).degree (cutoff s P.card) C x) := by
…

Mentions: OAI.WeakPinned.Theta, OAI.WeakPinned.Plane, OAI.WeakPinned.cutoff, OAI.WeakPinned.planarFibers

lemma OAI.WeakPinned.restricted_size_lt_card line 367
lemma OAI.WeakPinned.heavySubset_zero line 383

theorem OAI.WeakPinned.heavySubset_uniform line 398

Source documentation

A uniform extremal bound valid even for tiny subsets: their contribution is zero, rather than an uncontrolled diagonal error.

theorem heavySubset_uniform (P : Finset Plane) (s K lam r B : ℝ) (C D : Finset P)
    (hlam : 0 ≤ lam) (hB : 0 ≤ B) (m₁ : ℕ) (hm1 : 2 ≤ m₁)
    (hT : (m₁ : ℝ) ≤ lam*K)
    (hthreshold : (D.card : ℝ)^r ≤ lam*K)
    (hext : ∀ m : ℕ, m₁ ≤ m → m ≤ P.card → F m r ≤ B) :
    (∑ e, if heavyFiber P s K lam C D e ∧ (planarFibers P s).source e ∈ D
      then ((planarFibers P s).size D e : ℝ) else 0) ≤
      B*(D.card : ℝ)*((D.card : ℝ)-1) := by
…

Mentions: OAI.WeakPinned.Plane, OAI.WeakPinned.B, OAI.WeakPinned.F, OAI.WeakPinned.heavyFiber, OAI.WeakPinned.planarFibers

lemma OAI.WeakPinned.eventual_power_below_logsquare line 423
def OAI.WeakPinned.heavyCount line 447
structure OAI.WeakPinned.PreparedCore line 452
Source documentation
Uniform subset bounds for the finite planar core.
```
structure PreparedCore (s γ c η : ℝ) (P : Finset Plane) (C : Finset P) : Prop where
…
```
Mentions: OAI.WeakPinned.Plane
lemma OAI.WeakPinned.choose_above_critical line 469
lemma OAI.WeakPinned.log_cutoff_comparison line 479
theorem OAI.WeakPinned.arbitrarily_large_prepared line 492
Source documentation
Uniformity of both subset estimates is obtained before passing to any arithmetic model. Tiny subsets are treated exactly, with no diagonal error.
```
theorem arbitrarily_large_prepared (hfail : ¬ MainStatement) {s γ c : ℝ}
    (hγ : 0 < γ) (hγs : γ < s) (_hc : 0 < c) (hc1 : c < 1)
    (hsc : (1-c)*criticalExponent < s) (hs : ContinuousAt Theta s)
    (η : ℝ) (hη : 0 < η) (M : ℕ) :
    ∃ (P : Finset Plane) (C : Finset P), M < C.card ∧ PreparedCore s γ c η P C := by
…
```
Mentions: OAI.WeakPinned.MainStatement, OAI.WeakPinned.criticalExponent, OAI.WeakPinned.Theta, OAI.WeakPinned.Plane, OAI.WeakPinned.PreparedCore