LabelSwitches1.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SignedDisk.LabelSwitches.active line 30
Source documentation
Whether a switch has occurred since the most recent exceptional level.
```
def active (bad sw : ℕ → Bool) : ℕ → Bool
  | 0 => false
  | n+1 => if bad n then false else active bad sw n || sw n
```
def OAI.SignedDisk.LabelSwitches.count line 34
lemma OAI.SignedDisk.LabelSwitches.active_witness line 36
theorem OAI.SignedDisk.LabelSwitches.count_le line 58

theorem OAI.SignedDisk.LabelSwitches.count_energy line 90

Source documentation

Quantitative energy version. The exceptional set is the union of marks and levels with energy exceeding c. This includes an arbitrary birth offset.

theorem count_energy (mark sw : ℕ → Bool) (E : ℕ → ℝ) (n : ℕ) {c : ℝ}
    (hc : 0 < c) (hE : ∀ i < n, 0 ≤ E i)
    (hsep : ∀ i j, i < j → j < n → sw i = true → sw j = true →
      ∃ k, i ≤ k ∧ k ≤ j ∧ (mark k = true ∨ c < E k)) :
    ((count sw n : ℕ) : ℝ) ≤ 1+2*((count mark n : ℕ) : ℝ)+(2/c)*∑ i ∈ range n, E i := by
…

Mentions: OAI.SignedDisk.LabelSwitches.count

lemma OAI.SignedDisk.PlanePotential.green_eq_zero_of_outside line 130
Source documentation
The global segment kernel vanishes off the region on which the actual finite density decomposition is valid.
```
lemma green_eq_zero_of_outside {ψ : ℂ → ℝ} {R X : ℝ}
    (hs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hRX : R ≤ X) {x y : ℂ}
    (hx : ‖x‖ ≤ X) (hy : X < ‖y‖) : green ψ x y = 0 := by
…
```
Mentions: OAI.SignedDisk.PlanePotential.green
lemma OAI.SignedDisk.PlanePotential.green_gradient_representation line 152
theorem OAI.SignedDisk.PlanePotential.green_finite_decomposition line 159

theorem OAI.SignedDisk.PlanePotential.green_decomposition_norm line 182

Source documentation

The complete finite Minkowski step, after genuine kernel insertion.

theorem green_decomposition_norm {ι : Type*} [Fintype ι]
    {ψ g : ℂ → ℝ} (hψ : Continuous ψ) (hψc : HasCompactSupport ψ)
    (hg : ContDiff ℝ 1 g) {D R X Y B : ℝ}
    (hD : ∀ y, ‖fderiv ℝ g y‖ ≤ D) (hψ1 : ∫ z, ψ z = 1)
    (hψs : ∀ z, ψ z ≠ 0 → ‖z‖ ≤ R) (hψB : ∀ z, |ψ z| ≤ B)
    (hRX : R ≤ X) (hM : 0 < R+X) (hB : 0 ≤ B) (hXY : 0 < X+Y)
    (β : ι → ℂ → ℂ) (hβ : ∀ i, Integrable (β i))
    (hβs : ∀ i y, β i y ≠ 0 → ‖y‖ ≤ Y)
    (hdecomp : ∀ᵐ y, ‖y‖ ≤ X → gradient g y = ∑ i, β i y) :
    eLpNorm (fun x => g x-∫ z, ψ z*g z) (3/2) (volume.restrict {x : ℂ | ‖x‖ ≤ X}) ≤
      ∑ i, eLpNorm (fun x => ∫ y, ⟪green ψ x y,β i y⟫) (3/2)
        (volume.restrict {x : ℂ | ‖x‖ ≤ X}) := by
…

Mentions: OAI.SignedDisk.PlanePotential.green

def OAI.SignedDisk.RadiusEnvelope.envelope line 215
Source documentation
The signed envelope over the entire compact real-radius interval.
```
def envelope (u : ℝ → E → ℝ) (a b : ℝ) (x : E) : ℝ :=
…
```
lemma OAI.SignedDisk.RadiusEnvelope.attains line 218
lemma OAI.SignedDisk.RadiusEnvelope.le_envelope line 230
lemma OAI.SignedDisk.RadiusEnvelope.lipschitz line 236
lemma OAI.SignedDisk.RadiusEnvelope.zero_of_all_zero line 259

theorem OAI.SignedDisk.RadiusEnvelope.fderiv_touching line 267

Source documentation

Differentiable touching holds for every attaining radius; no derivative of an argmax selector is taken.

theorem fderiv_touching [NormedAddCommGroup E] [NormedSpace ℝ E] {u : ℝ → E → ℝ} {a b r : ℝ} {x : E}
    (hr : r ∈ Icc a b) (hc : ∀ y, ContinuousOn (fun t => u t y) (Icc a b))
    (he : envelope u a b x = u r x)
    (hd : DifferentiableAt ℝ (envelope u a b) x) (hu : DifferentiableAt ℝ (u r) x) :
    fderiv ℝ (envelope u a b) x = fderiv ℝ (u r) x := by
…

Mentions: OAI.SignedDisk.RadiusEnvelope.envelope

lemma OAI.SignedDisk.DiskMoments.signedAverage_lipschitz line 285
lemma OAI.SignedDisk.DiskMoments.signedAverage_radius_continuousOn line 309
lemma OAI.SignedDisk.DiskMoments.hasFDerivAt_signedAverage line 315
theorem OAI.SignedDisk.DiskMoments.run_envelope_lipschitz line 339
Source documentation
Actual signed run envelopes: locally differentiable almost everywhere, over all radii in their compact interval.
```
theorem run_envelope_lipschitz {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
    (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    ∃ L : ℝ≥0, LipschitzWith L (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) := by
…
```
Mentions: OAI.SignedDisk.RadiusEnvelope.envelope, OAI.SignedDisk.DiskMoments.signedAverage
lemma OAI.SignedDisk.DiskMoments.signedAverage_eq_zero_of_outside line 346
theorem OAI.SignedDisk.DiskMoments.run_envelope_hasCompactSupport line 362
Source documentation
Every radius in the run is retained, but a common compact spatial support still exists.
```
theorem run_envelope_hasCompactSupport {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
    (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    HasCompactSupport (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) := by
…
```
Mentions: OAI.SignedDisk.RadiusEnvelope.envelope, OAI.SignedDisk.DiskMoments.signedAverage

theorem OAI.SignedDisk.DiskMoments.run_envelope_ae_touching line 381

Source documentation

AE differentiability and universal touching of actual run gradients.

theorem run_envelope_ae_touching {g : ℂ → ℝ} (hg : ContDiff ℝ 1 g)
    (hgc : HasCompactSupport g) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    ∀ᵐ x, ∀ r ∈ Icc a b,
      RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b x = signedAverage g x r →
      fderiv ℝ (RadiusEnvelope.envelope (fun r x => signedAverage g x r) a b) x =
        (1/Real.pi) • ∫ z in Metric.ball 0 1, fderiv ℝ g (x+r • z) := by
…

Mentions: OAI.SignedDisk.RadiusEnvelope.envelope, OAI.SignedDisk.DiskMoments.signedAverage