OAI/Analysis/LipschitzHilbert/Trees/SourcePathProduct.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite path-product argument in §10. Marked indices retain the residual-free predictor; all consecutive unary runs use one common cubic variation estimate. The remaining unmarked large-drop index is unique. The estimates are independent of the number of angular levels.

  1. theorem OAI.LipschitzHilbert.UnaryRunPartition.indices_disjoint line 23
  2. theorem OAI.LipschitzHilbert.UnaryRunPartition.indices_union line 33
  3. theorem OAI.LipschitzHilbert.UnaryRunPartition.sum_runs line 52
  4. theorem OAI.LipschitzHilbert.UnaryRunPartition.sum_segments line 60
  5. theorem OAI.LipschitzHilbert.source_unary_runs_weighted_drop line 83

    Source documentation

    The discarded-top contributions sum against true relative drops, also when the unary indices have many separate consecutive runs.

    theorem source_unary_runs_weighted_drop {unary : ℕ → Prop} {n : ℕ → ℝ}
    {start finish : ℕ} (R : UnaryRunPartition unary start finish)
    (P : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2)
    (hn : Antitone n) {μ Q : ℝ} (hμ : μ ≤ 1)
    (hnpos : ∀ j ∈ Finset.Ico start finish, 0 < n j)
    (hQ : ∀ j ∈ Finset.Ico start finish, n j^μ ≤ Q) :
    (∑ i : UnaryRunSegment R P,
      n i.2.val.1^(μ-1)*(n i.2.val.1-n i.2.val.2)) ≤
        Q*∑ j ∈ (Finset.Ico start finish).filter unary, pathDrop n j := by
…

    Mentions: OAI.LipschitzHilbert.UnaryRunPartition, OAI.LipschitzHilbert.UnarySegmentPartition, OAI.LipschitzHilbert.UnaryRunSegment, OAI.LipschitzHilbert.pathDrop

  6. theorem OAI.LipschitzHilbert.source_unary_segment_log_cost line 119

    Source documentation

    Reindex the actual unary energy telescope to an arbitrary segment. The propagated comparison amplitude is required only on that segment.

    theorem source_unary_segment_log_cost {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] (n : ℕ → ℝ) (A Astar : ℕ → E) (beta : ℕ → ℝ)
    {e f : ℕ} {a p D : ℝ} (hef : e ≤ f)
    (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p) (hD : 0 ≤ D)
    (hstart : 4 ≤ n e) (hn : Antitone n) (hdrop : n e-n f ≤ 2)
    (hcontraction : ∀ j ∈ Finset.Ico e f, ‖Astar j‖ ≤ ‖Astar (j+1)‖)
    (hend : Astar f = A f) (hbeta : ∀ j ∈ Finset.Ico e f, 0 < beta j)
    (hprediction : ∀ j ∈ Finset.Ico e f, beta j ≤
      vertexAmount (n j) (A j) a p /
        (n j-n (j+1)+vertexAmount (n (j+1)) (A (j+1)) a p))
    (herror : ∀ j ∈ Finset.Icc e f, ‖A j-Astar j‖ ≤ D) :
    (∑ j ∈ Finset.Ico e f, Real.log (beta j)) ≤ 4*p*n e^((a-1)/p-1)*D := by
…

    Mentions: OAI.LipschitzHilbert.vertexAmount

  7. theorem OAI.LipschitzHilbert.source_unary_runs_log_cost line 153

    Source documentation

    All unary runs use one cubic-variation budget. The local error bound is the actual propagated amplitude error from Abel summation, not a hypothesis about the path product.

    theorem source_unary_runs_log_cost {unary : ℕ → Prop} {n : ℕ → ℝ}
    {start finish : ℕ} (R : UnaryRunPartition unary start finish)
    (P : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2)
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
    (A : ℕ → E) (Astar : ℕ → ℕ → ℕ → E) (beta : ℕ → ℝ)
    (profile : ℕ → F) (level : ℕ → ℕ) (hlevel : StrictMono level) (N : ℕ)
    (hendlevel : level finish ≤ N) (hn : Antitone n)
    {a p c M V C ε Q : ℝ} (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p)
    (hc : 0 < c) (hc1 : c ≤ 1) (hM : 4 ≤ M) (hμ : (a-1)/p ≤ 1/12)
    (hV : 0 ≤ V) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hmass : ∀ j ∈ (Finset.Ico start finish).filter unary, M ≤ n j)
    (hnpos : ∀ j ∈ Finset.Ico start finish, 0 < n j)
…

    Mentions: OAI.LipschitzHilbert.UnaryRunPartition, OAI.LipschitzHilbert.UnarySegmentPartition

  8. theorem OAI.LipschitzHilbert.source_unary_propagated_log_cost line 231

    Source documentation

    The comparison amplitudes used above can be the literal products of the path coefficients and the endpoint amplitude. This discharges their contraction and endpoint conditions from the true unary recurrence.

    theorem source_unary_propagated_log_cost {unary : ℕ → Prop} {n : ℕ → ℝ}
    {start finish : ℕ} (R : UnaryRunPartition unary start finish)
    (P : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2)
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E]
    [NormedAddCommGroup F] (A U W : ℕ → E) (coeff : ℕ → ℂ) (beta : ℕ → ℝ)
    (profile : ℕ → F) (level : ℕ → ℕ) (hlevel : StrictMono level) (N : ℕ)
    (hendlevel : level finish ≤ N) (hn : Antitone n)
    {a p c M V C ε Q : ℝ} (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p)
    (hc : 0 < c) (hc1 : c ≤ 1) (hM : 4 ≤ M) (hμ : (a-1)/p ≤ 1/12)
    (hV : 0 ≤ V) (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hmass : ∀ j ∈ (Finset.Ico start finish).filter unary, M ≤ n j)
    (hnpos : ∀ j ∈ Finset.Ico start finish, 0 < n j)
…

    Mentions: OAI.LipschitzHilbert.UnaryRunPartition, OAI.LipschitzHilbert.UnarySegmentPartition

  9. theorem OAI.LipschitzHilbert.source_exceptional_factor_le line 292

    Source documentation

    The exceptional factor is controlled just by its amplitude and the baseline mass in its denominator.

    theorem source_exceptional_factor_le {E : Type*} [NormedAddCommGroup E]
    (A : E) {n denominator M C a p : ℝ}
    (hn : 0 < n) (hden : n ≤ denominator) (hM : n ≤ M+1)
    (hC : 0 ≤ C) (ha : 1 ≤ a) (hp : 0 ≤ p) (hA : ‖A‖ ≤ C*n) :
    vertexAmount n A a p/denominator ≤ 1+C^p*(M+1)^(a-1) := by
…

    Mentions: OAI.LipschitzHilbert.vertexAmount

  10. theorem OAI.LipschitzHilbert.source_path_product_of_log_costs line 321

    Source documentation

    Split a finite active product into marked, unary and exceptional indices. The exceptional contribution costs once, even if its logarithm is negative.

    theorem source_path_product_of_log_costs (count : ℕ) (marked unary exceptional : ℕ → Prop)
    (beta beta0 : ℕ → ℝ) (markedCost unaryCost exceptionalCost : ℝ)
    (hbeta : ∀ j < count, 0 < beta j) (hbeta0 : ∀ j < count, marked j → 0 < beta0 j)
    (hpartition : ∀ j < count,
      (marked j ∨ unary j ∨ exceptional j) ∧
        ¬(marked j ∧ unary j) ∧ ¬(marked j ∧ exceptional j) ∧ ¬(unary j ∧ exceptional j))
    (hmarked : (∑ j ∈ (Finset.range count).filter marked,
      (Real.log (beta j)-Real.log (beta0 j))) ≤ markedCost)
    (hunary : (∑ j ∈ (Finset.range count).filter unary, Real.log (beta j)) ≤ unaryCost)
    (hexceptional : Set.Subsingleton {j | j < count ∧ exceptional j})
    (hcost : 0 ≤ exceptionalCost)
    (hexbound : ∀ j < count, exceptional j → Real.log (beta j) ≤ exceptionalCost) :
…
  11. theorem OAI.LipschitzHilbert.source_marked_log_cost line 396

    Source documentation

    The exact marked correction for the parent amplitude and its literal residual-free value. The square sum is over the marked blocks only.

    theorem source_marked_log_cost {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (n : ℕ → ℝ) (hn : Antitone n) (S : Finset ℕ)
    (A residual : ℕ → E) (denominator : ℕ → ℝ)
    {a p c M B : ℝ} (hp : 1 ≤ p) (hc : 0 < c) (hM : 1 ≤ M)
    (hμ : (a-1)/p ≤ 1/12) (hB : 0 ≤ B)
    (hdrop : ∀ j ∈ S, c ≤ n j-n (j+1))
    (hmass : ∀ j ∈ S, M ≤ n j) (hden : ∀ j ∈ S, 0 < denominator j)
    (hsquare : (∑ j ∈ S, ‖residual j‖^2) ≤ B^2) :
    (∑ j ∈ S, (Real.log (vertexAmount (n j) (A j) a p/denominator j)-
      Real.log (vertexAmount (n j) (A j-residual j) a p/denominator j))) ≤
      p*Real.sqrt (2*(1+3/c))*M^(-(1/2:ℝ)+(a-1)/p)*B := by
…

    Mentions: OAI.LipschitzHilbert.vertexAmount

  12. theorem OAI.LipschitzHilbert.source_path_product_from_vertex_costs line 414

    Source documentation

    Actual vertex ratios admit the finite source path bound. The unary cost is supplied by source_unary_runs_log_cost; the marked cost and unique exceptional factor are proved here from their local data.

    theorem source_path_product_from_vertex_costs
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (count : ℕ) (n : ℕ → ℝ) (A residual : ℕ → E) (denominator : ℕ → ℝ)
    (marked : ℕ → Prop) {a p c M B U C : ℝ}
    (hn : Antitone n) (hp : 1 ≤ p) (ha : 1 ≤ a) (hc : 0 < c)
    (hM : 1 ≤ M) (hμ : (a-1)/p ≤ 1/12) (hB : 0 ≤ B) (hC : 0 ≤ C)
    (hactive : ∀ j < count, M < n j)
    (hden : ∀ j < count, n j ≤ denominator j)
    (hdrop : ∀ j < count, marked j → c ≤ n j-n (j+1))
    (hsquare : (∑ j ∈ (Finset.range count).filter marked, ‖residual j‖^2) ≤ B^2)
    (hunary : (∑ j ∈ (Finset.range count).filter
      (fun j => ¬marked j ∧ n j-n (j+1) < 1),
…
  13. theorem OAI.LipschitzHilbert.source_path_product_from_propagated_residuals line 483

    Source documentation

    Assemble the full finite active path directly from residual square sums, the common cubic variation, and the actual propagated recurrence. The only interval hypothesis is the Abel bound on the propagated main residuals. It is imposed on unary intervals of total drop below two, exactly the intervals constructed in the proof.

    theorem source_path_product_from_propagated_residuals
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E]
    [NormedAddCommGroup F]
    (count : ℕ) (n : ℕ → ℝ) (A U W residual : ℕ → E)
    (coeff : ℕ → ℂ) (denominator : ℕ → ℝ) (marked : ℕ → Prop)
    (profile : ℕ → F) (level : ℕ → ℕ) (hlevel : StrictMono level) (N : ℕ)
    (hendlevel : level count ≤ N) (hn : Antitone n)
    {a p c M B V C ε Q Cex : ℝ}
    (hp : 1 ≤ p) (ha : 1 ≤ a) (hap : a ≤ p) (hc : 0 < c) (hc1 : c ≤ 1)
    (hM : 4 ≤ M) (hμ : (a-1)/p ≤ 1/12)
    (hB : 0 ≤ B) (hV : 0 ≤ V) (hC : 0 ≤ C) (hε : 0 ≤ ε) (hCex : 0 ≤ Cex)
    (hactive : ∀ j < count, M < n j)
…