BoundaryEnergy.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Finite sesquilinear tensor change of coordinates. The real change of variables assumption is explicit and is proved for the actual Jacobian.

lemma OAI.ElasticityBoundaryTensorPull.sum_four_exchange line 12
lemma OAI.ElasticityBoundaryTensorPull.sesqui_pull line 24
abbrev OAI.Elasticity.CMatrix line 43
def OAI.Elasticity.tensorDensity line 45
def OAI.Elasticity.sesquiDensity line 48
lemma OAI.Elasticity.complexDensity_sesqui line 52
lemma OAI.Elasticity.tensorDensity_isotropic line 62
lemma OAI.Elasticity.complexDensity_tensor line 70
abbrev OAI.ElasticityBoundaryDensityPull.I line 87
abbrev OAI.ElasticityBoundaryDensityPull.X line 88
abbrev OAI.ElasticityBoundaryDensityPull.Y line 89
def OAI.ElasticityBoundaryDensityPull.pullMatrix line 91
def OAI.ElasticityBoundaryDensityPull.pullTensor line 94
lemma OAI.ElasticityBoundaryDensityPull.tensor_pull line 98
lemma OAI.ElasticityBoundaryDensityPull.principal_pullTensor line 106
lemma OAI.ElasticityBoundaryDensityPull.gradient_pullMatrix line 122
lemma OAI.ElasticityBoundaryDensityPull.density_chart line 139
lemma OAI.ElasticityBoundaryDensityPull.tensor_zero_left line 167
lemma OAI.ElasticityBoundaryDensityPull.physical_density_support line 170
lemma OAI.ElasticityBoundaryDensityPull.chart_density_support line 180
lemma OAI.ElasticityBoundaryDensityPull.density_chart_all line 192

theorem OAI.ElasticityBoundaryEnergyChart.compact_chart_integral_complex line 229

Source documentation

A compactly supported physical integrand pulls back with its exact Jacobian, including the domain's half-space indicator.

theorem compact_chart_integral_complex (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (⊤ : ℕ∞) e e.source)
    {K Ω H : Set E} (hs : K⊆e.source) (hΩ : MeasurableSet Ω) (hH : MeasurableSet H)
    (hhalf : ∀ y∈e.source, e y∈Ω ↔ y∈H)
    {Φ : E → E} (hΦ : ∀ y∈K, Φ =ᶠ[𝓝 y] e)
    (f g : E → ℂ) (hf : Function.support f⊆e '' K) (hg : Function.support g⊆K)
    (hfg : ∀ y∈e.source, f (e y)=g y) :
    (∫ x in Ω, f x ∂μ)=(∫ y in H, |(fderiv ℝ Φ y).det| • g y ∂μ) := by
…

def OAI.ElasticityBoundaryPacket.Setup.jacobian line 279
def OAI.ElasticityBoundaryPacket.Setup.rawCoeff line 282
lemma OAI.ElasticityBoundaryPacket.Setup.jacobian_continuous line 285
lemma OAI.ElasticityBoundaryPacket.Setup.jacobian_pos line 289
lemma OAI.ElasticityBoundaryPacket.Setup.rawCoeff_continuous line 296
lemma OAI.ElasticityBoundaryPacket.Setup.rawCoeff_zero line 303

lemma OAI.ElasticityBoundaryPacket.Setup.compact_energy_coefficients line 309

Source documentation

All modifications of this coefficient are outside the support of the actual trial gradients. Its leading coefficient is the actual isotropic tensor.

lemma Setup.compact_energy_coefficients (s : Setup Ω x) {l m : X → ℂ}
    (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m) :
    ∃ H : I → I → I → I → Y → ℂ,
      (∀ i α j β, Continuous (H i α j β)) ∧
      (∀ i α j β, HasCompactSupport (H i α j β)) ∧
      (∀ i α j β y, WithLp.toLp 2 y∈s.K → H i α j β y=s.rawCoeff l m i α j β y) := by
…

Mentions: OAI.ElasticityBoundaryPacket.Setup, OAI.ElasticityBoundaryPacket.X, OAI.ElasticityBoundaryPacket.I, OAI.ElasticityBoundaryPacket.Y

abbrev OAI.ElasticityBoundaryLimit.Y line 341
lemma OAI.ElasticityBoundaryLimit.eventually_small_positive line 343
lemma OAI.ElasticityBoundaryLimit.OrderBound.conj line 348

theorem OAI.ElasticityBoundaryLimit.weighted_tendsto line 355

Source documentation

Domination uses the full Gaussian-normal weight, and is uniform for every small positive scale. No convergence of the physical DN symbol is assumed.

theorem weighted_tendsto {F : ℝ → Y → ℂ} {f : Y → ℂ}
    (hF : OrderBound F 0) (hc : ∀ δ, Continuous (F δ))
    (ht : ∀ y, Tendsto (fun δ => F δ y) (𝓝[>] 0) (𝓝 (f y)))
    {b : ℝ} (hb : 0<b) :
    Tendsto (fun δ => ∫ y, weight b y • F δ y) (𝓝[>] 0) (𝓝 (∫ y, weight b y • f y)) := by
…

Mentions: OAI.ElasticityBoundaryLimit.Y

lemma OAI.ElasticityBoundaryLimit.continuous_value_parameter line 380
lemma OAI.ElasticityBoundaryLimit.value_parameter_zero line 394
lemma OAI.ElasticityBoundaryLimit.PD_coeff_zero line 398
lemma OAI.ElasticityBoundaryLimit.firstScaled_tendsto line 402
lemma OAI.ElasticityBoundaryLimit.amplitude_coeff_zero line 418
abbrev OAI.ElasticityBoundaryEnergyLimit.Y line 434
lemma OAI.ElasticityBoundaryEnergyLimit.normal_power_bound line 436
def OAI.ElasticityBoundaryEnergyLimit.mixedScaled line 441
lemma OAI.ElasticityBoundaryEnergyLimit.mixed_scaled_bound line 445
lemma OAI.ElasticityBoundaryEnergyLimit.mixed_scaled_continuous line 452

theorem OAI.ElasticityBoundaryEnergyLimit.mixed_scaled_limit line 461

Source documentation

The coefficient at the base point is extracted from the exact mixed boundary energy. Corrections of every positive parameter order disappear.

theorem mixed_scaled_limit (n : ℕ) {H χ : Y → ℂ} (hH : Continuous H) (hcH : HasCompactSupport H)
    (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hcχ : HasCompactSupport χ) (h0 : χ 0=1)
    (p q : Polynomial W) (i α j β : Fin 3) :
    Tendsto (fun δ => ∫ y, weight 2 y • mixedScaled n H χ p q i α j β δ y) (𝓝[>] 0)
      (𝓝 (∫ y : Y, weight 2 y • ((y 2:ℂ)^n*H 0*
        value (E₀ α (p.coeff 0 i)) y*star (value (E₀ β (q.coeff 0 j)) y)))) := by
…

Mentions: OAI.ElasticityBoundaryEnergyLimit.Y, OAI.ElasticityBoundaryEnergyLimit.mixedScaled

abbrev OAI.ElasticityBoundaryMixedScaling.Y line 488
lemma OAI.ElasticityBoundaryMixedScaling.envelope_product_weight line 490
lemma OAI.ElasticityBoundaryMixedScaling.integral_envelope_mixed line 503
def OAI.ElasticityBoundaryMixedScaling.mixedEnergy line 509

theorem OAI.ElasticityBoundaryMixedScaling.mixedEnergy_scaled line 516

Source documentation

The factor delta^(2n) comes from the true normal coordinate, while the volume delta^4 cancels the two true first derivatives delta^-2.

theorem mixedEnergy_scaled (n : ℕ) (H : Y → ℂ) {χ : Y → ℂ}
    (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (p q : Polynomial W) (i α j β : Fin 3)
    {δ : ℝ} (hδ : δ≠0) :
    ((δ^(2*n))⁻¹:ℝ) • mixedEnergy n H χ p q i α j β δ=
      ∫ y, weight 2 y • mixedScaled n H χ p q i α j β δ y := by
…

Mentions: OAI.ElasticityBoundaryMixedScaling.Y, OAI.ElasticityBoundaryMixedScaling.mixedEnergy

theorem OAI.ElasticityBoundaryMixedScaling.mixedEnergy_limit line 540
lemma OAI.ElasticityBoundaryPacket.Setup.energy_chart line 564
lemma OAI.ElasticityBoundaryPacket.Setup.energy_compact_tensor line 600
lemma OAI.ElasticityBoundaryPacket.Setup.energy_sum line 622
lemma OAI.ElasticityBoundaryPacket.mixed_integrable line 660
lemma OAI.ElasticityBoundaryPacket.Setup.energy_difference_normal line 669
lemma OAI.ElasticityBoundaryPacket.normalized_tendsto_zero line 720
def OAI.ElasticityBoundaryPacket.frozenPair line 733

lemma OAI.ElasticityBoundaryPacket.Setup.extract_normal line 740

Source documentation

Any actual normal factor of the pulled tensor is detected. The hypothesis is an exact factorization on the packet support, not a boundary agreement assumption and not an abstract conclusion-carrying jet interface.

lemma Setup.extract_normal (s : Setup Ω x) {l₁ m₁ l₂ m₂ : X → ℝ}
    (hl₁ : ContDiff ℝ (⊤ : ℕ∞) l₁) (hm₁ : ContDiff ℝ (⊤ : ℕ∞) m₁)
    (hl₂ : ContDiff ℝ (⊤ : ℕ∞) l₂) (hm₂ : ContDiff ℝ (⊤ : ℕ∞) m₂)
    (ha₁ : Admissible Ω l₁ m₁) (ha₂ : Admissible Ω l₂ m₂)
    (hO : IsOpen Ω) (hB : Bornology.IsBounded Ω) (hx : x∈closure Ω)
    (hDN : DN Ω l₁ m₁=DN Ω l₂ m₂)
    (n : ℕ) (H : I → I → I → I → Y → ℂ)
    (hHc : ∀ i α j β, Continuous (H i α j β))
    (hHs : ∀ i α j β, HasCompactSupport (H i α j β))
    (hH : ∀ i α j β y, WithLp.toLp 2 y∈s.K →
      s.rawCoeff (fun z => (l₁ z:ℂ)) (fun z => (m₁ z:ℂ)) i α j β y-
      s.rawCoeff (fun z => (l₂ z:ℂ)) (fun z => (m₂ z:ℂ)) i α j β y=(y 2:ℂ)^n*H i α j β y)
…

Mentions: OAI.ElasticityBoundaryPacket.Setup, OAI.ElasticityBoundaryPacket.X, OAI.ElasticityBoundaryPacket.I, OAI.ElasticityBoundaryPacket.Y