AngularEnvelopeGraph.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual profile graph estimate on the admissible energy envelope

Restriction to a child is implemented by the existing spatial cell symbol. The original restricted endpoint integral is unchanged, and the support condition is propagated explicitly to the child's good set.

def OAI.Falconer.finiteEnvelopeMaximum line 17
theorem OAI.Falconer.finiteEnvelopeMaximum_nonneg line 20
theorem OAI.Falconer.le_finiteEnvelopeMaximum line 24
theorem OAI.Falconer.finiteEnvelopeMaximum_le line 28
theorem OAI.Falconer.angularEnvelope_le_of_admissible line 38
theorem OAI.Falconer.AngularAdmissible.cell line 53
theorem OAI.Falconer.child_energy_le_angularEnvelope line 65
theorem OAI.Falconer.profile_angular_envelope_terminal line 85

def OAI.Falconer.childAngularEnvelopeMaximum line 104

Source documentation

The finite maximum uses the same original measures and the actual child good sets.

noncomputable def childAngularEnvelopeMaximum {n : ℕ}
    (Q₁ Q₂ : DyadicCube (n+2)) (ρ₁ ρ₂ : Measure (Space (n+2))) (j : ℕ)
    (M P : ℝ) (k : ℕ) (D a v : ℝ) (Ψ : ℝ → ℝ)
    (GoodLeft GoodRight : List (Fin (n+2) → Bool) →
      Set (Space (n+2) × Sphere (n+2))) : ℝ :=
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere

theorem OAI.Falconer.profile_near_le_child_angular_envelope line 116

Source documentation

The actual near contribution uses the same finite child maximum as the graph step.

theorem profile_near_le_child_angular_envelope {n k : ℕ} (D : ℝ) (hD : 0 ≤ D)
    (Q : DyadicCube (n+2)) (hQ : Q.side = 1) (ρ : Measure (Space (n+2)))
    {m : ℝ → ℝ} {N : ℕ} {s lam : ℝ}
    (hreg : Regularization.RegularizedProfileData Q ρ N s lam m) (hN : 0 < N)
    {a p : ℕ} (hap : a ≤ p) (hp : p ≤ N)
    (X Y : List (Fin (n+2) → Bool)) (hX : X.length = a) (hY : Y.length = a)
    (v : ℝ) (Ψ : ℝ → ℝ)
    [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure v Ψ)]
    (GoodLeft GoodRight : Set (Space (n+2) × Sphere (n+2)))
    (ChildLeft ChildRight : List (Fin (n+2) → Bool) →
      Set (Space (n+2) × Sphere (n+2)))
    (hLeft : ∀ q ∈ (Q.descendant X).occupiedPaths ρ (p-a),
…

Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Regularization.RegularizedProfileData, OAI.PlanarFalconer.sourceAngularShellMeasure, OAI.Falconer.Sphere

theorem OAI.Falconer.dyadic_profile_angular_envelope_step line 161

Source documentation

The graph estimate preserves the fixed symbol budget in the parent and child suprema. Only the localization estimate uses the enlarged analytic budget.

theorem dyadic_profile_angular_envelope_step
    (hpublished : PublishedGnomonicSurface) (n k : ℕ) (hn : 1 ≤ n)
    (φ : 𝓢(ℝ, ℂ)) (Ψ : ℝ → ℝ)
    (hφ : ∀ u, φ u = (Ψ u : ℂ)) (hΨ : Measurable Ψ)
    (hpos : ∀ u, 0 ≤ Ψ u) (hzero : ∀ u ≤ 0, Ψ u = 0)
    {W : ℝ} (hW : 0 ≤ W) (hΨW : ∀ t, Ψ t ≤ W)
    (hsupp : ∀ t, Ψ t ≠ 0 → t ∈ Ioo (1/4 : ℝ) 4)
    {α : ℝ} (hα : 0 < α) (T : ℝ) :
    ∃ A C : ℝ, 0 ≤ A ∧ 0 < C ∧
      ∀ (Q₁ Q₂ : DyadicCube (n+2)), Q₁.side = 1 → Q₂.side = 1 →
      ∀ (ρ₁ ρ₂ : Measure (Space (n+2))) (N : ℕ) (s₁ s₂ lam : ℝ)
        (m₁ m₂ : ℝ → ℝ),
…

Mentions: OAI.Falconer.PublishedGnomonicSurface, OAI.Falconer.DyadicCube, OAI.Falconer.Space