PlaneEnvelopes.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.MovingHyperplaneChart.chart line 14
Source documentation
Projection onto an affine hyperplane along a fixed transverse direction.
```
def chart (v n : V) (c : ℝ) (z : V) : V :=
…
```
theorem OAI.Problem358.MovingHyperplaneChart.chart_mem line 18
Source documentation
The chart takes values in its target plane whenever the direction is transverse.
```
theorem chart_mem (v n : V) (c : ℝ) (z : V) (h : inner ℝ v n ≠ 0) :
    inner ℝ (chart v n c z) n + c = 0 := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart
theorem OAI.Problem358.MovingHyperplaneChart.chart_eq_self line 25
Source documentation
A point already on the target plane is fixed.
```
theorem chart_eq_self {v n z : V} {c : ℝ} (hz : inner ℝ z n + c = 0) :
    chart v n c z = z := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart
theorem OAI.Problem358.MovingHyperplaneChart.chart_add_smul line 30
Source documentation
Projection is invariant under translation parallel to its direction.
```
theorem chart_add_smul (v n : V) (c a : ℝ) (z : V) (h : inner ℝ v n ≠ 0) :
    chart v n c (z + a • v) = chart v n c z := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart
theorem OAI.Problem358.MovingHyperplaneChart.chart_chart line 41
Source documentation
Two successive charts with the same transverse direction collapse to the last one.
```
theorem chart_chart (v n₁ n₂ : V) (c₁ c₂ : ℝ) (z : V)
    (h₂ : inner ℝ v n₂ ≠ 0) :
    chart v n₂ c₂ (chart v n₁ c₁ z) = chart v n₂ c₂ z := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart
theorem OAI.Problem358.MovingHyperplaneChart.inverse_chart line 49
Source documentation
A reverse chart recovers every point of the original plane.
```
theorem inverse_chart {v n₀ n z : V} {c₀ c : ℝ}
    (h₀ : inner ℝ v n₀ ≠ 0) (hz : inner ℝ z n₀ + c₀ = 0) :
    chart v n₀ c₀ (chart v n c z) = z := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart
theorem OAI.Problem358.MovingHyperplaneChart.chart_injOn line 56
Source documentation
Restricting the chart to a plane transverse to its direction is injective.
```
theorem chart_injOn {v n₀ n : V} {c₀ c : ℝ} (h₀ : inner ℝ v n₀ ≠ 0) :
    Set.InjOn (chart v n c) {z | inner ℝ z n₀ + c₀ = 0} := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.MovingHyperplaneChart.chart_bijOn line 63

Source documentation

The chart maps one transverse plane onto the other.

theorem chart_bijOn {v n₀ n : V} {c₀ c : ℝ}
    (h₀ : inner ℝ v n₀ ≠ 0) (h : inner ℝ v n ≠ 0) :
    Set.BijOn (chart v n c) {z | inner ℝ z n₀ + c₀ = 0}
      {z | inner ℝ z n + c = 0} := by
…

Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.MovingHyperplaneChart.continuous_chart line 73
Source documentation
For fixed plane parameters the chart is a continuous affine map.
```
theorem continuous_chart (v n : V) (c : ℝ) : Continuous (chart v n c) := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart

def OAI.Problem358.MovingHyperplaneChart.planeHomeomorph line 78

Source documentation

The geometric identification of any two planes transverse to the same direction.

def planeHomeomorph (v n₀ n : V) (c₀ c : ℝ)
    (h₀ : inner ℝ v n₀ ≠ 0) (h : inner ℝ v n ≠ 0) :
    {z : V // inner ℝ z n₀ + c₀ = 0} ≃ₜ {z : V // inner ℝ z n + c = 0} where
…

theorem OAI.Problem358.MovingHyperplaneChart.continuousAt_chart_joint line 89
Source documentation
Joint continuity in the varying plane and the original point.
```
theorem continuousAt_chart_joint (v : V) {p : (V × ℝ) × V}
    (h : inner ℝ v p.1.1 ≠ 0) :
    ContinuousAt (fun q : (V × ℝ) × V => chart v q.1.1 q.1.2 q.2) p := by
…
```
Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.MovingHyperplaneChart.norm_chart_sub_le line 96

Source documentation

A uniform quantitative estimate for the moving chart on a bounded part of the old plane.

theorem norm_chart_sub_le {v n₀ n z : V} {c₀ c R : ℝ}
    (hz : inner ℝ z n₀ + c₀ = 0) (hR : ‖z‖ ≤ R) :
    ‖chart v n c z - z‖ ≤
      ((R * ‖n - n₀‖ + |c - c₀|) / |inner ℝ v n|) * ‖v‖ := by
…

Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.MovingHyperplaneChart.tendstoUniformlyOn_chart line 120

Source documentation

Nearby affine planes converge uniformly on every bounded part of the original plane.

theorem tendstoUniformlyOn_chart {v n₀ : V} {c₀ R : ℝ} {S : Set V}
    (h₀ : inner ℝ v n₀ ≠ 0)
    (hplane : ∀ z ∈ S, inner ℝ z n₀ + c₀ = 0)
    (hR : ∀ z ∈ S, ‖z‖ ≤ R) :
    TendstoUniformlyOn (fun p : V × ℝ => chart v p.1 p.2) id (𝓝 (n₀, c₀)) S := by
…

Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.MovingHyperplaneChart.tendstoUniformlyOn_chart_of_isCompact line 144

Source documentation

Compact parts of the original plane satisfy the uniform convergence statement.

theorem tendstoUniformlyOn_chart_of_isCompact {v n₀ : V} {c₀ : ℝ} {S : Set V}
    (h₀ : inner ℝ v n₀ ≠ 0) (hS : IsCompact S)
    (hplane : ∀ z ∈ S, inner ℝ z n₀ + c₀ = 0) :
    TendstoUniformlyOn (fun p : V × ℝ => chart v p.1 p.2) id (𝓝 (n₀, c₀)) S := by
…

Mentions: OAI.Problem358.MovingHyperplaneChart.chart

theorem OAI.Problem358.TangentEnvelope.norm_tangent_le_two_radius line 166
Source documentation
Orthogonal projection bounds the tangent coordinate independently of the normal displacement used to straighten a moving face.
```
theorem norm_tangent_le_two_radius {u z w : V} {t R : ℝ}
    (horth : ⟪w, u⟫ = 0) (hz : ‖z‖ ≤ R)
    (hx : ‖z + w + t • u‖ ≤ R) : ‖w‖ ≤ 2 * R := by
…
```

theorem OAI.Problem358.TangentEnvelope.tangent_mem_closedBall_of_mem line 181

Source documentation

A body inside a radius-R ball pulls back to a fixed radius-2R support in tangent coordinates, uniformly for every normal displacement.

theorem tangent_mem_closedBall_of_mem {u z : V} {K : Set V} {R t : ℝ}
    (hK : ∀ x ∈ K, ‖x‖ ≤ R) (hz : z ∈ K)
    (w : (ℝ ∙ u)ᗮ) (hx : z + (w : V) + t • u ∈ K) :
    w ∈ closedBall (0 : (ℝ ∙ u)ᗮ) (2 * R) := by
…

theorem OAI.Problem358.TangentEnvelope.norm_body_indicator_le_tangent_envelope line 192

Source documentation

A bounded test function restricted to the source body has one compact surface envelope valid for all moving-strip normal coordinates.

theorem norm_body_indicator_le_tangent_envelope {F : Type*}
    [NormedAddCommGroup F] {u z : V} {K : Set V} {R B t : ℝ}
    (hK : ∀ x ∈ K, ‖x‖ ≤ R) (hz : z ∈ K) (hB : 0 ≤ B)
    {f : V → F} (hf : ∀ x ∈ K, ‖f x‖ ≤ B) (w : (ℝ ∙ u)ᗮ) :
    ‖K.indicator f (z + (w : V) + t • u)‖ ≤
      (closedBall (0 : (ℝ ∙ u)ᗮ) (2 * R)).indicator (fun _ => B) w := by
…

theorem OAI.Problem358.TangentEnvelope.integrable_tangent_polynomial_envelope line 208

Source documentation

Polynomially growing speeds times a compact tangent cutoff are integrable. This supplies the domination required by moving-boundary differentiation.

theorem integrable_tangent_polynomial_envelope [FiniteDimensional ℝ V]
    [MeasurableSpace V] [BorelSpace V] (u : V)
    (μ : Measure ((ℝ ∙ u)ᗮ)) [μ.IsAddHaarMeasure]
    (R A B : ℝ) (n : ℕ) :
    Integrable ((closedBall (0 : (ℝ ∙ u)ᗮ) R).indicator
      (fun w => (A + B * ‖w‖) ^ n)) μ := by
…

abbrev OAI.Problem358.MovingPlaneEnvelope.Plane line 233
Source documentation
The fixed reference plane, with its induced topology and measurable structure.
```
abbrev Plane (n₀ : V) (c₀ : ℝ) := {z : V // inner ℝ z n₀ + c₀ = 0}
```
def OAI.Problem358.MovingPlaneEnvelope.projection line 236
Source documentation
Projection back to the fixed reference plane along the common transverse direction.
```
def projection (v n₀ : V) (c₀ : ℝ) (h₀ : inner ℝ v n₀ ≠ 0) (z : V) : Plane n₀ c₀ :=
…
```
Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane
theorem OAI.Problem358.MovingPlaneEnvelope.continuous_projection line 239
def OAI.Problem358.MovingPlaneEnvelope.envelope line 244
Source documentation
A compact set produces one compact envelope on the reference plane.
```
def envelope (v n₀ : V) (c₀ : ℝ) (h₀ : inner ℝ v n₀ ≠ 0) (K : Set V) :
    Set (Plane n₀ c₀) := projection v n₀ c₀ h₀ '' K
```
Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane, OAI.Problem358.MovingPlaneEnvelope.projection
theorem OAI.Problem358.MovingPlaneEnvelope.isCompact_envelope line 247
theorem OAI.Problem358.MovingPlaneEnvelope.chart_preimage_subset_envelope line 253
Source documentation
Every moving-plane pullback of K is contained in the same compact envelope. No bound on the moving normal or intercept, nor moving transversality, is needed.
```
theorem chart_preimage_subset_envelope {v n₀ : V} {c₀ : ℝ}
    (h₀ : inner ℝ v n₀ ≠ 0) (K : Set V) (n : V) (c : ℝ) :
    {z : Plane n₀ c₀ | chart v n c z.val ∈ K} ⊆ envelope v n₀ c₀ h₀ K := by
…
```
Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane, OAI.Problem358.MovingPlaneEnvelope.envelope

theorem OAI.Problem358.MovingPlaneEnvelope.norm_indicator_chart_le line 263

Source documentation

A bounded integrand cut off on K has a parameter-independent indicator bound when pulled back by any moving-plane chart.

theorem norm_indicator_chart_le {W : Type*} [NormedAddCommGroup W]
    {v n₀ : V} {c₀ : ℝ} (h₀ : inner ℝ v n₀ ≠ 0)
    {K : Set V} {g : V → W} {C : ℝ} (hC : 0 ≤ C)
    (hg : ∀ x ∈ K, ‖g x‖ ≤ C) (n : V) (c : ℝ) (z : Plane n₀ c₀) :
    ‖K.indicator g (chart v n c z.val)‖ ≤
      (envelope v n₀ c₀ h₀ K).indicator (fun _ => C) z := by
…

Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane, OAI.Problem358.MovingPlaneEnvelope.envelope

theorem OAI.Problem358.MovingPlaneEnvelope.norm_smul_indicator_chart_le line 277

Source documentation

Extra cell-cut factors bounded by one do not change the common envelope.

theorem norm_smul_indicator_chart_le {W : Type*} [NormedAddCommGroup W]
    [NormedSpace ℝ W] {v n₀ : V} {c₀ : ℝ} (h₀ : inner ℝ v n₀ ≠ 0)
    {K : Set V} {g : V → W} {C : ℝ} (hC : 0 ≤ C)
    (hg : ∀ x ∈ K, ‖g x‖ ≤ C) (n : V) (c : ℝ) (z : Plane n₀ c₀)
    (a : ℝ) (ha : |a| ≤ 1) :
    ‖a • K.indicator g (chart v n c z.val)‖ ≤
      (envelope v n₀ c₀ h₀ K).indicator (fun _ => C) z := by
…

Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane, OAI.Problem358.MovingPlaneEnvelope.envelope

theorem OAI.Problem358.MovingPlaneEnvelope.integrable_envelope_bound line 293
Source documentation
Local finiteness on the reference plane makes the fixed compact envelope integrable.
```
theorem integrable_envelope_bound {K : Set V} (hK : IsCompact K) (C : ℝ) :
    Integrable ((envelope v n₀ c₀ h₀ K).indicator (fun _ => C)) μ := by
…
```
Mentions: OAI.Problem358.MovingPlaneEnvelope.envelope

theorem OAI.Problem358.MovingPlaneEnvelope.exists_integrable_chart_majorant line 301

Source documentation

Continuous tests on a compact body admit one integrable majorant for every moving chart and every additional scalar cut factor of absolute value at most one.

theorem exists_integrable_chart_majorant {W : Type*} [NormedAddCommGroup W]
    [NormedSpace ℝ W] {K : Set V} (hK : IsCompact K) {g : V → W}
    (hg : ContinuousOn g K) :
    ∃ B : Plane n₀ c₀ → ℝ, Integrable B μ ∧ (∀ z, 0 ≤ B z) ∧
      ∀ (n : V) (c : ℝ) (z : Plane n₀ c₀) (a : ℝ), |a| ≤ 1 →
        ‖a • K.indicator g (chart v n c z.val)‖ ≤ B z := by
…

Mentions: OAI.Problem358.MovingPlaneEnvelope.Plane