ResidualMeans.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Point density and mean bounds for the two strip residual test functions.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity_perm line 15
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity_eq_zero_of_not_injective line 31

lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pointDensity_bound_of_sorted line 43

Source documentation

Sorting is legitimate for the actual product of the two, possibly nonsymmetric, evaluation determinants: both acquire the same sign.

lemma pointDensity_bound_of_sorted {n : ℕ} (w w₁ w₂ : ℝ → ℝ) (F G R : Fin n → ℝ → ℝ)
    (A B : ℝ)
    (hb : ∀ p : Fin n → ℝ,StrictMono p → (∀ i,0<p i) →
      familyPointDensity w R G p ≤ A*familyPointDensity w₁ F G p+B*familyPointDensity w₂ F G p) :
    ∀ p : Fin n → ℝ,(∀ i,0<p i) →
      familyPointDensity w R G p ≤ A*familyPointDensity w₁ F G p+B*familyPointDensity w₂ F G p := by
…

Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity

lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelOriginFunctional_eq_residual_det line 62
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalized_residual_density line 80
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPoleProduct line 99
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingProduct line 101
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPoleProduct_pos line 104
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPoleProduct_le_one line 107
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingProduct_ge_one line 115
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPole_prefix_good line 121
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingProduct_prefix_bad line 161
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPole_prefix_bound line 183
Source documentation
A deterministic ordered-node estimate converting the first-N pole product to the full characteristic product, with a moving-parameter error.
```
lemma fixedPole_prefix_bound {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) (x : ℕ  →  ℝ) {u c T : ℝ}
    (hx : ∀ i,0 < x i) (hu : 0 ≤ u) (hc : 0 < c) (huc : u ≤ c) (hT : 0 < T)
    (hord : Monotone (fun i : Fin n => x i)) :
    fixedPoleProduct x u c m  ≤  (1+c/T)^n*fixedPoleProduct x u c n+
      (2/3:ℝ)^m*movingProduct x T n := by
…
```
Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedPoleProduct, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingProduct
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJetFamily line 213
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeExtension line 215
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeExtension_fin line 217
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeExtension_pos line 219
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeExtension_prod line 224
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalFixedWeight line 229
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalMovingWeight line 230
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physical_pole_product line 232
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_positiveEvaluation line 239
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_residual_density_bound line 245
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_point_density_upper line 301
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_point_density_upper line 314
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_pair_integrable line 337
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_characteristic_pair_integrable line 344
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_sq_real line 357
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_sq_real line 363
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_sq_unit line 368
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_sq_unit line 375
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.bounded_target_stripJet_integrable line 388
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_stripJet_integrable line 409
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_stripJet_integrable line 418
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalFixedWeight_characteristic line 437
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physicalMovingWeight_characteristic line 443
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_gram_det_pos line 449
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetFixedMean line 455
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetMovingMean line 458
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_residual_mean_upper line 462
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_mean_upper line 485
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_mean_upper line 494
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pointDensity_lower_of_sorted line 513
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_lower line 531
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_residual_density_lower line 553
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_residual_mean_lower line 590
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_mean_lower line 606
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_mean_lower line 612