OAI/Analysis/CircleDomains/Rigidity/TraceMaskLinePayment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual mask primitive inherits line payment from its scalar cutoffs. Finite interval-length sums are dominated by the density before passing to the infinite mask; no differentiability of minima is used.

  1. theorem OAI.CircleDomainRigidity.infiniteTracePrimitive_lipschitz line 14
  2. theorem OAI.CircleDomainRigidity.trace_primitive_line_payment line 27
  3. theorem OAI.CircleDomainRigidity.masked_scalar_increment line 64
  4. theorem OAI.CircleDomainRigidity.masked_scalar_ACL_of_line_payment line 79
  5. theorem OAI.CircleDomainRigidity.masked_scalar_derivative_of_line_payment line 102

    Source documentation

    The same payment bounds the actual derivative almost everywhere.

     theorem masked_scalar_derivative_of_line_payment
    {cutoff : ℕ → ℝ → ℝ} (hc : ∀ j x, cutoff j x ∈ Icc (0:ℝ) 1)
    {I : ℕ → Set ℝ} (hI : ∀ j, MeasurableSet (I j)) (hIf : ∀ j, volume (I j) ≠ ∞)
    {g : ℕ → ℝ → ℝ} {P Q b : ℝ → ℝ} {L R : ℝ} (hLR : L ≤ R)
    (hg : ∀ j, IntervalIntegrable (g j) volume L R)
    (hP : IntervalIntegrable P volume L R) (hQ : IntervalIntegrable Q volume L R)
    (hnonneg : ∀ᵐ x ∂volume.restrict (Icc L R), 0 ≤ Q x+P x)
    (hcut : ∀ j, ∀ x ∈ uIcc L R, ∀ y ∈ uIcc L R,
      |cutoff j x-cutoff j y| ≤ ∫ s in uIoc x y, g j s)
    (hdom : ∀ n s, s ∈ uIcc L R →
      ∑ j ∈ Finset.range n, volume.real (I j)*g j s ≤ P s)
    (hb : ∀ x ∈ uIcc L R, ∀ y ∈ uIcc L R, |b x-b y| ≤ ∫ s in uIoc x y, Q s)
…