OAI/Analysis/LipschitzHilbert/Trees/SourcePlaneWeightCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The source plane integral already has the exact top-weight mass. The marked-path and conditional-average exponentials combine into a fixed constant, independent of all packet and top scales.

  1. theorem OAI.LipschitzHilbert.source_plane_weight_cost line 12
  2. theorem OAI.LipschitzHilbert.source_plane_bound_by_weight line 21

    Source documentation

    The spatial estimate is exactly the weight integral required by the finite-tree moment theorem; it has no residual area normalization.

    theorem source_plane_bound_by_weight (T : SlopeBox) (K D cost I : ℝ) (hK : 0 < K)
    (h : I ≤ (((Real.exp 3*cost)*(Real.exp 1*Real.exp (2*D)))*
      (2^D*∫ z, topProfile D z ∂volume.prod volume))*K^2*T.length*T.width) :
    I ≤ Real.exp (4+2*D)*cost*(∫ z, T.weight K D z ∂volume.prod volume) :=
…

    Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.topProfile